Package stream-thm: Properties of stream types
Information
| name | stream-thm |
| version | 1.17 |
| description | Properties of stream types |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-08-11 |
| requires | bool function list natural pair stream-def |
| show | Data.Bool Data.List Data.Pair Data.Stream Function Number.Natural |
Files
- Package tarball stream-thm-1.17.tgz
- Theory file stream-thm.thy (included in the package tarball)
Theorems
⊦ map id = id
⊦ ∀s. [] @ s = s
⊦ ∀s. drop s 0 = s
⊦ ∀s. drop s 1 = tail s
⊦ ∀h t. head (h :: t) = h
⊦ ∀h t. tail (h :: t) = t
⊦ ∀s n. length (take s n) = n
⊦ ∀h t. nth (h :: t) 0 = h
⊦ ∀s. take s 1 = head s :: []
⊦ ∀s n. drop s n = (tail ↑ n) s
⊦ ∀s n. head (drop s n) = nth s n
⊦ ∀s1 s2. split (interleave s1 s2) = (s1, s2)
⊦ ∀s n. nth s (suc n) = nth (tail s) n
⊦ ∀s n. drop s (suc n) = tail (drop s n)
⊦ ∀s n. drop s (suc n) = drop (tail s) n
⊦ ∀f g. map f ∘ map g = map (f ∘ g)
⊦ ∀h t n. nth (h :: t) (suc n) = nth t n
⊦ ∀h t s. (h :: t) @ s = h :: t @ s
⊦ ∀l1 l2 s. (l1 @ l2) @ s = l1 @ l2 @ s
⊦ ∀s m n. nth s (m + n) = nth (drop s n) m
⊦ ∀s1 s2. (∀n. nth s1 n = nth s2 n) ⇒ s1 = s2
⊦ ∀f g s. map (f ∘ g) s = map f (map g s)
⊦ ∀s n. take s (suc n) = take s n @ nth s n :: []
⊦ ∀s m n. take s (m + n) = take s m @ take (drop s m) n
⊦ ∀f b. unfold f b = let (a, b') ← f b in a :: unfold f b'
⊦ ∀l s n.
nth (l @ s) n = if n < length l then nth l n else nth s (n - length l)
⊦ ∀p.
(∀m. ∃n. m ≤ n ∧ p n) ⇒
∃s. (∀i j. nth s i ≤ nth s j ⇔ i ≤ j) ∧ ∀n. p n ⇔ ∃i. nth s i = n
Input Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- Stream
- stream
- List
- Number
- Natural
- natural
- Natural
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- length
- nth
- Pair
- ,
- fst
- snd
- Stream
- ::
- @
- drop
- fromFunction
- head
- interleave
- map
- nth
- split
- tail
- take
- unfold
- Bool
- Function
- ↑
- id
- ∘
- Number
- Natural
- *
- +
- -
- <
- ≤
- bit0
- bit1
- div
- even
- minimal
- mod
- odd
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ length [] = 0
⊦ bit0 0 = 0
⊦ ∀t. t ⇒ t
⊦ ∀n. 0 ≤ n
⊦ ⊥ ⇔ ∀p. p
⊦ ∀x. id x = x
⊦ ∀t. t ∨ ¬t
⊦ ∀m. ¬(m < 0)
⊦ ∀n. n < suc n
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ ∀t. (t ⇔ ⊤) ⇔ t
⊦ ∀t. ⊥ ∧ t ⇔ ⊥
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. ⊥ ⇒ t ⇔ ⊤
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀t. ⊤ ∨ t ⇔ ⊤
⊦ ∀t. t ∨ ⊥ ⇔ t
⊦ ∀n. ¬(suc n = 0)
⊦ ∀n. 0 + n = n
⊦ ∀m. m + 0 = m
⊦ ∀m. m - 0 = m
⊦ ∀l. [] @ l = l
⊦ ∀s. take s 0 = []
⊦ ∀s. fromFunction (nth s) = s
⊦ ∀f. f ↑ 0 = id
⊦ ∀f. id ∘ f = f
⊦ ∀f. nth (fromFunction f) = f
⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t
⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t
⊦ ∀t. t ⇒ ⊥ ⇔ ¬t
⊦ ∀n. even (2 * n)
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ ∀n. ¬odd n ⇔ even n
⊦ ∀s. head s = nth s 0
⊦ ∀m n. m ≤ m + n
⊦ ∀m n. n ≤ m + n
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀n. odd (suc (2 * n))
⊦ ∀m. suc m = m + 1
⊦ ∀n. even (suc n) ⇔ ¬even n
⊦ ∀m. m ≤ 0 ⇔ m = 0
⊦ ∀n. suc n - 1 = n
⊦ ∀s. tail s = drop s 1
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀x y. fst (x, y) = x
⊦ ∀x y. snd (x, y) = y
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ ∀n. 0 < n ⇔ ¬(n = 0)
⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))
⊦ ∀xy. ∃x y. xy = (x, y)
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀h t. nth (h :: t) 0 = h
⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1
⊦ ∀m n. m * n = n * m
⊦ ∀m n. m + n - m = n
⊦ ∀n. 2 * n = n + n
⊦ ∀h t. length (h :: t) = suc (length t)
⊦ ∀m n. ¬(m < n ∧ n ≤ m)
⊦ ∀m n. ¬(m ≤ n ∧ n < m)
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. ¬(m ≤ n) ⇔ n < m
⊦ ∀m n. m < suc n ⇔ m ≤ n
⊦ ∀m n. suc m ≤ n ⇔ m < n
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ ∀p. (∀b. p b) ⇔ p ⊤ ∧ p ⊥
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀p. ¬(∀x. p x) ⇔ ∃x. ¬p x
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀t1 t2. ¬t1 ⇒ ¬t2 ⇔ t2 ⇒ t1
⊦ ∀m n. m + suc n = suc (m + n)
⊦ ∀m n. suc m + n = suc (m + n)
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀m n. suc m < suc n ⇔ m < n
⊦ ∀f s. map f s = fromFunction (f ∘ nth s)
⊦ ∀n. odd n ⇔ n mod 2 = 1
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀m n. even (m * n) ⇔ even m ∨ even n
⊦ ∀m n. even (m + n) ⇔ even m ⇔ even n
⊦ ∀l1 l2. length (l1 @ l2) = length l1 + length l2
⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d
⊦ ∀s n. drop s n = fromFunction (λm. nth s (m + n))
⊦ ∀f g. (∀x. f x = g x) ⇔ f = g
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n
⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n
⊦ ∀f. ∃fn. ∀x y. fn (x, y) = f x y
⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d
⊦ ∀p. (∀x y. p x y) ⇔ ∀y x. p x y
⊦ ∀p q. p ∧ (∃x. q x) ⇔ ∃x. p ∧ q x
⊦ ∀p q. p ∨ (∀x. q x) ⇔ ∀x. p ∨ q x
⊦ ∀p q. p ∨ (∃x. q x) ⇔ ∃x. p ∨ q x
⊦ ∀m n. ¬(m = 0) ⇒ m * n div m = n
⊦ ∀s n. take s (suc n) = head s :: take (tail s) n
⊦ ∀p q. (∃x. p x) ∧ q ⇔ ∃x. p x ∧ q
⊦ ∀p q. (∃x. p x) ⇒ q ⇔ ∀x. p x ⇒ q
⊦ ∀p q. (∃x. p x) ∨ q ⇔ ∃x. p x ∨ q
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀m n p. m + p = n + p ⇔ m = n
⊦ ∀m n p. m + n < m + p ⇔ n < p
⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p
⊦ ∀m n p. m < n ∧ n < p ⇒ m < p
⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p
⊦ ∀l h t. (h :: t) @ l = h :: t @ l
⊦ ∀f n x. (f ↑ suc n) x = f ((f ↑ n) x)
⊦ ∀f n x. (f ↑ suc n) x = (f ↑ n) (f x)
⊦ ∀f g h. f ∘ (g ∘ h) = f ∘ g ∘ h
⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n
⊦ ∀m n. m * n = 0 ⇔ m = 0 ∨ n = 0
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀f b. unfold f b = fromFunction (λn. fst (f (((snd ∘ f) ↑ n) b)))
⊦ ∀p. (∀n. (∀m. m < n ⇒ p m) ⇒ p n) ⇒ ∀n. p n
⊦ ∀p q. (∃x. p x) ∨ (∃x. q x) ⇔ ∃x. p x ∨ q x
⊦ ∀m n. ¬(n = 0) ⇒ (m div n) * n + m mod n = m
⊦ ∀h t n. n < length t ⇒ nth (h :: t) (suc n) = nth t n
⊦ ∀h t. h :: t = fromFunction (λn. if n = 0 then h else nth t (n - 1))
⊦ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p
⊦ ∀m n p. m * n ≤ m * p ⇔ m = 0 ∨ n ≤ p
⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m
⊦ ∀m n p. m * n < m * p ⇔ ¬(m = 0) ∧ n < p
⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b
⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)
⊦ ∀l s.
l @ s =
fromFunction
(λn. if n < length l then nth l n else nth s (n - length l))
⊦ ∀s1 s2.
interleave s1 s2 =
fromFunction
(λn. if even n then nth s1 (n div 2) else nth s2 (n div 2))
⊦ ∀s.
split s =
(fromFunction (λn. nth s (2 * n)),
fromFunction (λn. nth s (2 * n + 1)))
⊦ ∀l1 l2 k.
k < length l1 + length l2 ⇒
nth (l1 @ l2) k =
if k < length l1 then nth l1 k else nth l2 (k - length l1)