Package stream-def: Definition of infinite stream types

Information

namestream-def
version1.36
descriptionDefinition of infinite stream types
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-04
checksumd095373c35d2ddb55a8ceed5aba9350ef4518020
requiresbase
showData.Bool
Data.List
Data.Pair
Data.Stream
Function
Number.Natural

Files

Defined Type Operator

Defined Constants

Theorems

replicate = iterate id

s. take s 0 = []

s. fromFunction (nth s) = s

f. nth (fromFunction f) = f

s. head s = nth s 0

s. tail s = drop s 1

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

f s. map f s = fromFunction (f nth s)

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

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

f b. unfold f b = fromFunction (λn. fst (f (((snd f) n) b)))

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

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

External Type Operators

External Constants

Assumptions

() = λp. p ((select) p)

t. (x. t) t

t. (x. t) t

() = λp. p = λx.

t. ( t) t

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

(∃!) = λp. () p x y. p x p y x = y

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