src/HOLCF/ex/Stream.thy

Isar version of ZF/AC

(*  Title: 	HOLCF/ex/Stream.thy
    ID:         $Id$
    Author: 	Franz Regensburger, David von Oheimb
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

General Stream domain.
*)

Stream = HOLCF + Nat_Infinity +

domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65)

consts

  smap		:: "('a -> 'b) -> 'a stream -> 'b stream"
  sfilter	:: "('a -> tr) -> 'a stream -> 'a stream"
  slen		:: "'a stream => inat"			("#_" [1000] 1000)

defs

  smap_def	"smap	 == fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
  sfilter_def	"sfilter == fix\\<cdot>(\\<Lambda>h p s. case s of x && xs => 
				     If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)"
  slen_def	"#s == if stream_finite s 
		      then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>"

end