src/HOLCF/ex/Coind.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Coind.thy	Wed Jan 19 17:40:26 1994 +0100
@@ -0,0 +1,37 @@
+(*  Title: 	HOLCF/coind.thy
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Example for co-induction on streams
+*)
+
+Coind = Stream2 +
+
+
+consts
+
+nats		:: "dnat stream"
+from		:: "dnat -> dnat stream"
+
+rules
+
+nats_def	"nats = fix[LAM h.scons[dzero][smap[dsucc][h]]]"
+
+from_def	"from = fix[LAM h n.scons[n][h[dsucc[n]]]]"
+
+end
+
+(*
+
+		smap[f][UU] = UU
+      x~=UU --> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]
+
+		nats = scons[dzero][smap[dsucc][nats]]
+
+		from[n] = scons[n][from[dsucc[n]]]
+
+
+*)
+
+