Package stream: Stream types

Information

name	stream
version	1.32
description	Stream types
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool function list natural pair set
show	Data.Bool Data.List Data.Pair Data.Stream Function Number.Natural Set

Files

Package tarball stream-1.32.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

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

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

⊦ ∀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 x. member x (take s n) ⇔ ∃i. i < n ∧ x = nth s i

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

⊦ ∀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 ⇔ 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. even (suc n) ⇔ ¬even n

⊦ ∀m. m ≤ 0 ⇔ m = 0

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

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

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

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

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

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

⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)

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

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

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

⊦ (∃!) = λ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

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

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