isabelle: src/HOL/HOLCF/ex/Fix2.thy@89347c0cc6a3 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/ex/Fix2.thy
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	2	Author: Franz Regensburger
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	3
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	4	Show that fix is the unique least fixed-point operator.
12036 49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	5	From axioms gix1_def,gix2_def it follows that fix = gix
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Fix2
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports HOLCF
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11
25135 4f8176c940cf modernized specifications ('definition', 'axiomatization'); wenzelm parents: 19742 diff changeset	12	axiomatization
63549 b0d31c7def86 more symbols; wenzelm parents: 42151 diff changeset	13	gix :: "('a \<rightarrow> 'a) \<rightarrow>'a" where
b0d31c7def86 more symbols; wenzelm parents: 42151 diff changeset	14	gix1_def: "F\<cdot>(gix\<cdot>F) = gix\<cdot>F" and
b0d31c7def86 more symbols; wenzelm parents: 42151 diff changeset	15	gix2_def: "F\<cdot>y = y \<Longrightarrow> gix\<cdot>F << y"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	17
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	18	lemma lemma1: "fix = gix"
40002 c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 35174 diff changeset	19	apply (rule cfun_eqI)
40431 682d6c455670 discontinue a bunch of legacy theorem names huffman parents: 40002 diff changeset	20	apply (rule below_antisym)
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	21	apply (rule fix_least)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	22	apply (rule gix1_def)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	23	apply (rule gix2_def)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	24	apply (rule fix_eq [symmetric])
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	25	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	26
63549 b0d31c7def86 more symbols; wenzelm parents: 42151 diff changeset	27	lemma lemma2: "gix\<cdot>F = lub (range (\<lambda>i. iterate i\<cdot>F\<cdot>UU))"
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	28	apply (rule lemma1 [THEN subst])
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	29	apply (rule fix_def2)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	30	done
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	31
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	32	end

author	haftmann
	Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734	89347c0cc6a3
parent 63549	b0d31c7def86
permissions	-rw-r--r--