Package stream-def: Definition of stream types

Information

namestream-def
version1.19
descriptionDefinition of stream types
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-08-11
requiresbool
natural
showData.Bool
Data.List
Data.Pair
Data.Stream
Number.Natural

Files

Defined Type Operator

Defined Constants

Theorems

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 s. map f s = fromFunction (Function.∘ 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 (Function.↑ (Function.∘ 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)))

Input Type Operators

Input 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. (x. y. p x y) y. x. p x (y x)

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

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