isabelle: src/HOLCF/explicit_domains/Stream2.thy@23ceb1dc9755 (annotated)

1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	1	(*
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	2	ID: $Id$
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	3	Author: Franz Regensburger
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	Additional constants for stream
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	8
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	9	Stream2 = Stream +
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	10
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11	consts
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	13	smap :: "('a -> 'b) -> 'a stream -> 'b stream"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15	defs
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17	smap_def
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	18	"smap == fix`(LAM h f s. stream_when`(LAM x l.scons `(f`x) `(h`f`l)) `s)"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	19
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	20
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21	end
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	22
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	23
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	24	(*
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	25	smap`f`UU = UU
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	26	x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	27
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	28	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	29

author	paulson
	Thu, 18 Jan 1996 10:38:29 +0100
changeset 1444	23ceb1dc9755
parent 1274	ea0668a1c0ba
child 1479	21eb5e156d91
permissions	-rw-r--r--