17 ("Tools/datatype_abs_proofs.ML") |
17 ("Tools/datatype_abs_proofs.ML") |
18 ("Tools/datatype_case.ML") |
18 ("Tools/datatype_case.ML") |
19 ("Tools/datatype_package.ML") |
19 ("Tools/datatype_package.ML") |
20 ("Tools/primrec_package.ML") |
20 ("Tools/primrec_package.ML") |
21 begin |
21 begin |
|
22 |
|
23 subsection {* Least and greatest fixed points *} |
|
24 |
|
25 definition |
|
26 lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
27 "lfp f = Inf {u. f u \<le> u}" --{*least fixed point*} |
|
28 |
|
29 definition |
|
30 gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
31 "gfp f = Sup {u. u \<le> f u}" --{*greatest fixed point*} |
|
32 |
|
33 |
|
34 subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *} |
|
35 |
|
36 text{*@{term "lfp f"} is the least upper bound of |
|
37 the set @{term "{u. f(u) \<le> u}"} *} |
|
38 |
|
39 lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A" |
|
40 by (auto simp add: lfp_def intro: Inf_lower) |
|
41 |
|
42 lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f" |
|
43 by (auto simp add: lfp_def intro: Inf_greatest) |
|
44 |
|
45 lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f" |
|
46 by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) |
|
47 |
|
48 lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)" |
|
49 by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) |
|
50 |
|
51 lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)" |
|
52 by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) |
|
53 |
|
54 lemma lfp_const: "lfp (\<lambda>x. t) = t" |
|
55 by (rule lfp_unfold) (simp add:mono_def) |
|
56 |
|
57 |
|
58 subsection {* General induction rules for least fixed points *} |
|
59 |
|
60 theorem lfp_induct: |
|
61 assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P" |
|
62 shows "lfp f <= P" |
|
63 proof - |
|
64 have "inf (lfp f) P <= lfp f" by (rule inf_le1) |
|
65 with mono have "f (inf (lfp f) P) <= f (lfp f)" .. |
|
66 also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric]) |
|
67 finally have "f (inf (lfp f) P) <= lfp f" . |
|
68 from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI) |
|
69 hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound) |
|
70 also have "inf (lfp f) P <= P" by (rule inf_le2) |
|
71 finally show ?thesis . |
|
72 qed |
|
73 |
|
74 lemma lfp_induct_set: |
|
75 assumes lfp: "a: lfp(f)" |
|
76 and mono: "mono(f)" |
|
77 and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" |
|
78 shows "P(a)" |
|
79 by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) |
|
80 (auto simp: inf_set_eq intro: indhyp) |
|
81 |
|
82 lemma lfp_ordinal_induct: |
|
83 assumes mono: "mono f" |
|
84 and P_f: "!!S. P S ==> P(f S)" |
|
85 and P_Union: "!!M. !S:M. P S ==> P(Union M)" |
|
86 shows "P(lfp f)" |
|
87 proof - |
|
88 let ?M = "{S. S \<subseteq> lfp f & P S}" |
|
89 have "P (Union ?M)" using P_Union by simp |
|
90 also have "Union ?M = lfp f" |
|
91 proof |
|
92 show "Union ?M \<subseteq> lfp f" by blast |
|
93 hence "f (Union ?M) \<subseteq> f (lfp f)" by (rule mono [THEN monoD]) |
|
94 hence "f (Union ?M) \<subseteq> lfp f" using mono [THEN lfp_unfold] by simp |
|
95 hence "f (Union ?M) \<in> ?M" using P_f P_Union by simp |
|
96 hence "f (Union ?M) \<subseteq> Union ?M" by (rule Union_upper) |
|
97 thus "lfp f \<subseteq> Union ?M" by (rule lfp_lowerbound) |
|
98 qed |
|
99 finally show ?thesis . |
|
100 qed |
|
101 |
|
102 |
|
103 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, |
|
104 to control unfolding*} |
|
105 |
|
106 lemma def_lfp_unfold: "[| h==lfp(f); mono(f) |] ==> h = f(h)" |
|
107 by (auto intro!: lfp_unfold) |
|
108 |
|
109 lemma def_lfp_induct: |
|
110 "[| A == lfp(f); mono(f); |
|
111 f (inf A P) \<le> P |
|
112 |] ==> A \<le> P" |
|
113 by (blast intro: lfp_induct) |
|
114 |
|
115 lemma def_lfp_induct_set: |
|
116 "[| A == lfp(f); mono(f); a:A; |
|
117 !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) |
|
118 |] ==> P(a)" |
|
119 by (blast intro: lfp_induct_set) |
|
120 |
|
121 (*Monotonicity of lfp!*) |
|
122 lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g" |
|
123 by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans) |
|
124 |
|
125 |
|
126 subsection {* Proof of Knaster-Tarski Theorem using @{term gfp} *} |
|
127 |
|
128 text{*@{term "gfp f"} is the greatest lower bound of |
|
129 the set @{term "{u. u \<le> f(u)}"} *} |
|
130 |
|
131 lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f" |
|
132 by (auto simp add: gfp_def intro: Sup_upper) |
|
133 |
|
134 lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X" |
|
135 by (auto simp add: gfp_def intro: Sup_least) |
|
136 |
|
137 lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)" |
|
138 by (iprover intro: gfp_least order_trans monoD gfp_upperbound) |
|
139 |
|
140 lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f" |
|
141 by (iprover intro: gfp_lemma2 monoD gfp_upperbound) |
|
142 |
|
143 lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)" |
|
144 by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) |
|
145 |
|
146 |
|
147 subsection {* Coinduction rules for greatest fixed points *} |
|
148 |
|
149 text{*weak version*} |
|
150 lemma weak_coinduct: "[| a: X; X \<subseteq> f(X) |] ==> a : gfp(f)" |
|
151 by (rule gfp_upperbound [THEN subsetD], auto) |
|
152 |
|
153 lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f" |
|
154 apply (erule gfp_upperbound [THEN subsetD]) |
|
155 apply (erule imageI) |
|
156 done |
|
157 |
|
158 lemma coinduct_lemma: |
|
159 "[| X \<le> f (sup X (gfp f)); mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))" |
|
160 apply (frule gfp_lemma2) |
|
161 apply (drule mono_sup) |
|
162 apply (rule le_supI) |
|
163 apply assumption |
|
164 apply (rule order_trans) |
|
165 apply (rule order_trans) |
|
166 apply assumption |
|
167 apply (rule sup_ge2) |
|
168 apply assumption |
|
169 done |
|
170 |
|
171 text{*strong version, thanks to Coen and Frost*} |
|
172 lemma coinduct_set: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)" |
|
173 by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq]) |
|
174 |
|
175 lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)" |
|
176 apply (rule order_trans) |
|
177 apply (rule sup_ge1) |
|
178 apply (erule gfp_upperbound [OF coinduct_lemma]) |
|
179 apply assumption |
|
180 done |
|
181 |
|
182 lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))" |
|
183 by (blast dest: gfp_lemma2 mono_Un) |
|
184 |
|
185 |
|
186 subsection {* Even Stronger Coinduction Rule, by Martin Coen *} |
|
187 |
|
188 text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both |
|
189 @{term lfp} and @{term gfp}*} |
|
190 |
|
191 lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)" |
|
192 by (iprover intro: subset_refl monoI Un_mono monoD) |
|
193 |
|
194 lemma coinduct3_lemma: |
|
195 "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] |
|
196 ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))" |
|
197 apply (rule subset_trans) |
|
198 apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) |
|
199 apply (rule Un_least [THEN Un_least]) |
|
200 apply (rule subset_refl, assumption) |
|
201 apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) |
|
202 apply (rule monoD, assumption) |
|
203 apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) |
|
204 done |
|
205 |
|
206 lemma coinduct3: |
|
207 "[| mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)" |
|
208 apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) |
|
209 apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto) |
|
210 done |
|
211 |
|
212 |
|
213 text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, |
|
214 to control unfolding*} |
|
215 |
|
216 lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)" |
|
217 by (auto intro!: gfp_unfold) |
|
218 |
|
219 lemma def_coinduct: |
|
220 "[| A==gfp(f); mono(f); X \<le> f(sup X A) |] ==> X \<le> A" |
|
221 by (iprover intro!: coinduct) |
|
222 |
|
223 lemma def_coinduct_set: |
|
224 "[| A==gfp(f); mono(f); a:X; X \<subseteq> f(X Un A) |] ==> a: A" |
|
225 by (auto intro!: coinduct_set) |
|
226 |
|
227 (*The version used in the induction/coinduction package*) |
|
228 lemma def_Collect_coinduct: |
|
229 "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); |
|
230 a: X; !!z. z: X ==> P (X Un A) z |] ==> |
|
231 a : A" |
|
232 apply (erule def_coinduct_set, auto) |
|
233 done |
|
234 |
|
235 lemma def_coinduct3: |
|
236 "[| A==gfp(f); mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A" |
|
237 by (auto intro!: coinduct3) |
|
238 |
|
239 text{*Monotonicity of @{term gfp}!*} |
|
240 lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g" |
|
241 by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) |
|
242 |
22 |
243 |
23 subsection {* Inductive predicates and sets *} |
244 subsection {* Inductive predicates and sets *} |
24 |
245 |
25 text {* Inversion of injective functions. *} |
246 text {* Inversion of injective functions. *} |
26 |
247 |
62 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
283 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
63 not_all not_ex |
284 not_all not_ex |
64 Ball_def Bex_def |
285 Ball_def Bex_def |
65 induct_rulify_fallback |
286 induct_rulify_fallback |
66 |
287 |
|
288 ML {* |
|
289 val def_lfp_unfold = @{thm def_lfp_unfold} |
|
290 val def_gfp_unfold = @{thm def_gfp_unfold} |
|
291 val def_lfp_induct = @{thm def_lfp_induct} |
|
292 val def_coinduct = @{thm def_coinduct} |
|
293 val inf_bool_eq = @{thm inf_bool_eq} |
|
294 val inf_fun_eq = @{thm inf_fun_eq} |
|
295 val le_boolI = @{thm le_boolI} |
|
296 val le_boolI' = @{thm le_boolI'} |
|
297 val le_funI = @{thm le_funI} |
|
298 val le_boolE = @{thm le_boolE} |
|
299 val le_funE = @{thm le_funE} |
|
300 val le_boolD = @{thm le_boolD} |
|
301 val le_funD = @{thm le_funD} |
|
302 val le_bool_def = @{thm le_bool_def} |
|
303 val le_fun_def = @{thm le_fun_def} |
|
304 *} |
|
305 |
67 use "Tools/inductive_package.ML" |
306 use "Tools/inductive_package.ML" |
68 setup InductivePackage.setup |
307 setup InductivePackage.setup |
69 |
308 |
70 theorems [mono] = |
309 theorems [mono] = |
71 imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj |
310 imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj |
72 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
311 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
73 not_all not_ex |
312 not_all not_ex |
74 Ball_def Bex_def |
313 Ball_def Bex_def |
75 induct_rulify_fallback |
314 induct_rulify_fallback |
76 |
|
77 lemma False_meta_all: |
|
78 "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)" |
|
79 proof |
|
80 fix P |
|
81 assume False |
|
82 then show P .. |
|
83 next |
|
84 assume "\<And>P\<Colon>bool. P" |
|
85 then show False . |
|
86 qed |
|
87 |
|
88 lemma not_eq_False: |
|
89 assumes not_eq: "x \<noteq> y" |
|
90 and eq: "x \<equiv> y" |
|
91 shows False |
|
92 using not_eq eq by auto |
|
93 |
|
94 lemmas not_eq_quodlibet = |
|
95 not_eq_False [simplified False_meta_all] |
|
96 |
315 |
97 |
316 |
98 subsection {* Inductive datatypes and primitive recursion *} |
317 subsection {* Inductive datatypes and primitive recursion *} |
99 |
318 |
100 text {* Package setup. *} |
319 text {* Package setup. *} |