Package stream: Infinite stream types

Information

Files

• Package tarball stream-1.50.tgz
• Theory source file stream.thy (included in the package tarball)

Defined Type Operator

• Data
  • Stream
    • stream

Defined Constants

• Data
  • Stream
    • ::
    • @
    • drop
    • fromFunction
    • head
    • interleave
    • iterate
    • map
    • nth
    • replicate
    • split
    • tail
    • take
    • unfold

Theorems

⊦ replicate = iterate id

⊦ map id = id

⊦ ∀s. take s 0 = []

⊦ ∀s. fromFunction (nth s) = s

⊦ ∀s. [] @ s = s

⊦ ∀s. drop s 0 = s

⊦ ∀f. nth (fromFunction f) = f

⊦ ∀s. head s = nth s 0

⊦ ∀a. replicate a = a :: replicate a

⊦ ∀s. tail s = drop s 1

⊦ ∀s. drop s 1 = tail s

⊦ ∀a n. nth (replicate a) n = a

⊦ ∀h t. head (h :: t) = h

⊦ ∀h t. tail (h :: t) = t

⊦ ∀s n. length (take s n) = n

⊦ ∀s. nth s 1 = head (tail s)

⊦ ∀h t. nth (h :: t) 0 = h

⊦ ∀f. iterate f = unfold (λa. (a, f a))

⊦ ∀s. take s 1 = head s :: []

⊦ ∀s n. drop s n = (tail ↑ n) s

⊦ ∀s n. head (drop s n) = nth s n

⊦ ∀s₁ s₂. split (interleave s₁ s₂) = (s₁, s₂)

⊦ ∀f b. head (unfold f b) = fst (f b)

⊦ ∀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 s. map f s = fromFunction (f ∘ nth s)

⊦ ∀f a. iterate f a = a :: iterate f (f a)

⊦ ∀f g. map f ∘ map g = map (f ∘ g)

⊦ ∀f b. tail (unfold f b) = unfold f (snd (f b))

⊦ ∀s n. drop s n = fromFunction (λm. nth s (m + n))

⊦ ∀h t n. nth (h :: t) (suc n) = nth t n

⊦ ∀s n. take s (suc n) = head s :: take (tail s) n

⊦ ∀h t s. (h :: t) @ s = h :: t @ s

⊦ ∀l₁ l₂ s. (l₁ @ l₂) @ s = l₁ @ l₂ @ s

⊦ ∀s m n. nth s (m + n) = nth (drop s n) m

⊦ ∀s₁ s₂. (∀n. nth s₁ n = nth s₂ n) ⇔ s₁ = s₂

⊦ ∀s₁ s₂. (∀n. nth s₁ n = nth s₂ n) ⇒ s₁ = s₂

⊦ ∀f g s. map (f ∘ g) s = map f (map g s)

⊦ ∀f b. unfold f b = fromFunction (λn. fst (f (((snd ∘ f) ↑ n) b)))

⊦ ∀s n. take s (suc n) = take s n @ nth s n :: []

⊦ ∀s n i. i < n ⇒ nth (take s n) i = nth s i

⊦ ∀h t. h :: t = fromFunction (λn. if n = 0 then h else nth t (n - 1))

⊦ ∀s m n. take s (m + n) = take s m @ take (drop s m) n

⊦ ∀s n. nth s n = if n = 0 then head s else nth (tail s) (n - 1)

⊦ ∀s n x. member x (take s n) ⇔ ∃i. i < n ∧ x = nth s i

⊦ ∀s n. take s n = if n = 0 then [] else head s :: take (tail s) (n - 1)

⊦ ∀l s.
    l @ s =
    fromFunction
      (λn. if n < length l then nth l n else nth s (n - length l))

⊦ ∀f b. unfold f b = let (a, b') ← f b in a :: unfold f b'

⊦ ∀f b n k. nth (unfold f b) (n + k) = nth (unfold f (((snd ∘ f) ↑ n) b)) k

⊦ ∀l s n.
    nth (l @ s) n = if n < length l then nth l n else nth s (n - length l)

⊦ ∀s n. toSet (take s n) = { x. x | ∃i. i < n ∧ x = nth s i }

⊦ ∀s₁ s₂.
    interleave s₁ s₂ =
    fromFunction
      (λn. if even n then nth s₁ (n div 2) else nth s₂ (n div 2))

⊦ ∀s.
    split s =
    (fromFunction (λn. nth s (2 * n)),
     fromFunction (λn. nth s (2 * n + 1)))

⊦ ∀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

External Type Operators

• →
• bool
• Data
  • List
    • list
  • Pair
    • ×
• Number
  • Natural
    • natural
• Set
  • set

External Constants

• =
• select
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∃!
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • @
    • []
    • length
    • member
    • nth
    • toSet
  • Pair
    • ,
    • fst
    • snd
• Function
  • ↑
  • id
  • ∘
• Number
  • Natural
    • *
    • +
    • -
    • <
    • ≤
    • bit0
    • bit1
    • div
    • even
    • minimal
    • mod
    • odd
    • suc
    • zero
• Set
  • fromPredicate
  • ∈

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ length [] = 0

⊦ bit0 0 = 0

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ ∀x. ¬member x []

⊦ ∀x. id x = x

⊦ ∀t. t ∨ ¬t

⊦ ∀m. ¬(m < 0)

⊦ ∀n. ¬(n < n)

⊦ ∀n. 0 < suc n

⊦ ∀n. n < suc n

⊦ (¬) = λp. p ⇒ ⊥

⊦ (∃) = λp. p ((select) p)

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀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

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀m. m - 0 = m

⊦ ∀l. [] @ l = l

⊦ ∀f. f ↑ 0 = id

⊦ ∀f. id ∘ 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

⊦ ∀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. suc n - 1 = n

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀a b. fst (a, b) = a

⊦ ∀a b. snd (a, b) = b

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))

⊦ ∀f y. (let x ← y in f x) = f y

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀h t. nth (h :: t) 0 = h

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ ∀m n. m * n = n * m

⊦ ∀m n. m + n = n + m

⊦ ∀m n. m + n - m = n

⊦ ∀h t. length (h :: t) = suc (length t)

⊦ ∀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

⊦ ∀l x. member x l ⇔ x ∈ toSet l

⊦ ∀p. (∀b. p b) ⇔ p ⊤ ∧ p ⊥

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀p. ¬(∀x. p x) ⇔ ∃x. ¬p x

⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀t₁ t₂. ¬t₁ ⇒ ¬t₂ ⇔ t₂ ⇒ t₁

⊦ ∀m n. m + suc n = suc (m + n)

⊦ ∀m n. suc m + n = suc (m + n)

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀n. odd n ⇔ n mod 2 = 1

⊦ ∀f g x. (f ∘ g) x = f (g x)

⊦ ∀t₁ t₂. ¬(t₁ ∧ t₂) ⇔ ¬t₁ ∨ ¬t₂

⊦ ∀l₁ l₂. length (l₁ @ l₂) = length l₁ + length l₂

⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d

⊦ ∀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. ∀a b. fn (a, b) = f a b

⊦ ∀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

⊦ ∀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

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

⊦ ∀m n p. m + (n + p) = m + n + p

⊦ ∀p m n. 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

⊦ ∀s t. (∀x. x ∈ s ⇔ x ∈ t) ⇔ s = t

⊦ ∀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

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀p x. x ∈ { y. y | p y } ⇔ p x

⊦ ∀x h t. member x (h :: t) ⇔ x = h ∨ member x t

⊦ ∀f m n. f ↑ (m + n) = f ↑ m ∘ f ↑ n

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀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

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

⊦ ∀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

⊦ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p

⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m

⊦ ∀a b a' b'. (a, b) = (a', b') ⇔ a = a' ∧ b = b'

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀l₁ l₂ k.
    k < length l₁ + length l₂ ⇒
    nth (l₁ @ l₂) k =
    if k < length l₁ then nth l₁ k else nth l₂ (k - length l₁)

OpenTheory package document generated by opentheory 1.3 (release 20151025)