isabelle: src/HOLCF/ex/Fix2.thy@d539d47cce69 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/ex/Fix2.thy
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	4
12036 49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	5	Show that fix is the unique least fixed-point operator.
49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	6	From axioms gix1_def,gix2_def it follows that fix = gix
1274 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	Fix2 = Fix +
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	gix :: "('a->'a)->'a"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15	rules
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
10835 f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	17	gix1_def "F$(gix$F) = gix$F"
f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	18	gix2_def "F$y=y ==> gix$F << y"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	19
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	20	end

author	wenzelm
	Wed, 22 Jun 2005 19:41:29 +0200
changeset 16541	d539d47cce69
parent 14981	e73f8140af78
child 17291	94f6113fe9ed
permissions	-rw-r--r--