22 ("Tools/datatype_codegen.ML") |
22 ("Tools/datatype_codegen.ML") |
23 begin |
23 begin |
24 |
24 |
25 subsection {* Least and greatest fixed points *} |
25 subsection {* Least and greatest fixed points *} |
26 |
26 |
|
27 context complete_lattice |
|
28 begin |
|
29 |
27 definition |
30 definition |
28 lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where |
31 lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where |
29 "lfp f = Inf {u. f u \<le> u}" --{*least fixed point*} |
32 "lfp f = Inf {u. f u \<le> u}" --{*least fixed point*} |
30 |
33 |
31 definition |
34 definition |
32 gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where |
35 gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where |
33 "gfp f = Sup {u. u \<le> f u}" --{*greatest fixed point*} |
36 "gfp f = Sup {u. u \<le> f u}" --{*greatest fixed point*} |
34 |
37 |
35 |
38 |
36 subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *} |
39 subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *} |
37 |
40 |
41 lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A" |
44 lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A" |
42 by (auto simp add: lfp_def intro: Inf_lower) |
45 by (auto simp add: lfp_def intro: Inf_lower) |
43 |
46 |
44 lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f" |
47 lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f" |
45 by (auto simp add: lfp_def intro: Inf_greatest) |
48 by (auto simp add: lfp_def intro: Inf_greatest) |
|
49 |
|
50 end |
46 |
51 |
47 lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f" |
52 lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f" |
48 by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) |
53 by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) |
49 |
54 |
50 lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)" |
55 lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)" |
79 and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" |
84 and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" |
80 shows "P(a)" |
85 shows "P(a)" |
81 by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) |
86 by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) |
82 (auto simp: inf_set_eq intro: indhyp) |
87 (auto simp: inf_set_eq intro: indhyp) |
83 |
88 |
84 lemma lfp_ordinal_induct: |
89 lemma lfp_ordinal_induct: |
|
90 fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a" |
|
91 assumes mono: "mono f" |
|
92 and P_f: "\<And>S. P S \<Longrightarrow> P (f S)" |
|
93 and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)" |
|
94 shows "P (lfp f)" |
|
95 proof - |
|
96 let ?M = "{S. S \<le> lfp f \<and> P S}" |
|
97 have "P (Sup ?M)" using P_Union by simp |
|
98 also have "Sup ?M = lfp f" |
|
99 proof (rule antisym) |
|
100 show "Sup ?M \<le> lfp f" by (blast intro: Sup_least) |
|
101 hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD]) |
|
102 hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp |
|
103 hence "f (Sup ?M) \<in> ?M" using P_f P_Union by simp |
|
104 hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper) |
|
105 thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound) |
|
106 qed |
|
107 finally show ?thesis . |
|
108 qed |
|
109 |
|
110 lemma lfp_ordinal_induct_set: |
85 assumes mono: "mono f" |
111 assumes mono: "mono f" |
86 and P_f: "!!S. P S ==> P(f S)" |
112 and P_f: "!!S. P S ==> P(f S)" |
87 and P_Union: "!!M. !S:M. P S ==> P(Union M)" |
113 and P_Union: "!!M. !S:M. P S ==> P(Union M)" |
88 shows "P(lfp f)" |
114 shows "P(lfp f)" |
89 proof - |
115 using assms unfolding Sup_set_def [symmetric] |
90 let ?M = "{S. S \<subseteq> lfp f & P S}" |
116 by (rule lfp_ordinal_induct) |
91 have "P (Union ?M)" using P_Union by simp |
|
92 also have "Union ?M = lfp f" |
|
93 proof |
|
94 show "Union ?M \<subseteq> lfp f" by blast |
|
95 hence "f (Union ?M) \<subseteq> f (lfp f)" by (rule mono [THEN monoD]) |
|
96 hence "f (Union ?M) \<subseteq> lfp f" using mono [THEN lfp_unfold] by simp |
|
97 hence "f (Union ?M) \<in> ?M" using P_f P_Union by simp |
|
98 hence "f (Union ?M) \<subseteq> Union ?M" by (rule Union_upper) |
|
99 thus "lfp f \<subseteq> Union ?M" by (rule lfp_lowerbound) |
|
100 qed |
|
101 finally show ?thesis . |
|
102 qed |
|
103 |
117 |
104 |
118 |
105 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, |
119 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, |
106 to control unfolding*} |
120 to control unfolding*} |
107 |
121 |