isabelle: src/HOLCF/ex/Fix2.thy@59bd96046ad6 (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
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	4	Copyright 1995 Technische Universitaet Muenchen
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	Show that fix is the unique least fixed-point operator.
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7	From axioms gix1_def,gix2_def it follows that fix = gix
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	8
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	9	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	10
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11	Fix2 = Fix +
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	13	consts
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15	gix :: "('a->'a)->'a"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17	rules
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	18
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	19	gix1_def "F`(gix`F) = gix`F"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	20	gix2_def "F`y=y ==> gix`F << y"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	22	end

author	wenzelm
	Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754	59bd96046ad6
parent 2570	24d7e8fb8261
child 10835	f4745d77e620
permissions	-rw-r--r--