isabelle: src/HOLCF/ex/Coind.thy@7d6b0241afab (annotated)

244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	1	(* Title: HOLCF/coind.thy
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	2	ID: $Id$
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	3	Author: Franz Regensburger
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	5
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	6	Example for co-induction on streams
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	7	*)
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	8
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	9	Coind = Stream2 +
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	10
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	11
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	12	consts
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	13
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	14	nats :: "dnat stream"
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	15	from :: "dnat -> dnat stream"
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	16
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	17	defs
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	18	nats_def "nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))"
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	19
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	20	from_def "from == fix`(LAM h n.scons`n`(h`(dsucc`n)))"
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	21
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	22	end
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	23
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	24	(*
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	25	smap`f`UU = UU
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	26	x~=UU --> smap`f`(scons`x`xs) = scons`(f`x)`(smap`f`xs)
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	27
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	28	nats = scons`dzero`(smap`dsucc`nats)
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	29
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 244 diff changeset	30	from`n = scons`n`(from`(dsucc`n))
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	31	*)
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	32
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	33

author	paulson
	Mon, 14 Aug 1995 13:42:27 +0200
changeset 1228	7d6b0241afab
parent 1168	74be52691d62
permissions	-rw-r--r--