isabelle: src/HOLCF/ex/Fix2.thy@937baa077df2 (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
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	Show that fix is the unique least fixed-point operator.
12036 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
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	theory Fix2
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	imports HOLCF
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	11	begin
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
25135 4f8176c940cf modernized specifications ('definition', 'axiomatization'); wenzelm parents: 19742 diff changeset	13	axiomatization
4f8176c940cf modernized specifications ('definition', 'axiomatization'); wenzelm parents: 19742 diff changeset	14	gix :: "('a->'a)->'a" where
4f8176c940cf modernized specifications ('definition', 'axiomatization'); wenzelm parents: 19742 diff changeset	15	gix1_def: "F$(gix$F) = gix$F" and
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	16	gix2_def: "F$y=y ==> gix$F << y"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	18
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	19	lemma lemma1: "fix = gix"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	20	apply (rule ext_cfun)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	21	apply (rule antisym_less)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	22	apply (rule fix_least)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	23	apply (rule gix1_def)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	24	apply (rule gix2_def)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	25	apply (rule fix_eq [symmetric])
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	26	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	27
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	28	lemma lemma2: "gix$F=lub(range(%i. iterate i$F$UU))"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	29	apply (rule lemma1 [THEN subst])
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	30	apply (rule fix_def2)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	31	done
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	32
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	33	end

author	ballarin
	Mon, 19 Jan 2009 20:37:08 +0100
changeset 29566	937baa077df2
parent 25135	4f8176c940cf
child 35174	e15040ae75d7
permissions	-rw-r--r--