src/HOL/Inductive.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (23 months ago) changeset 67022 49309fe530fd parent 64674 ef0a5fd30f3b child 69593 3dda49e08b9d permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
1 (*  Title:      HOL/Inductive.thy
2     Author:     Markus Wenzel, TU Muenchen
3 *)
5 section \<open>Knaster-Tarski Fixpoint Theorem and inductive definitions\<close>
7 theory Inductive
8   imports Complete_Lattices Ctr_Sugar
9   keywords
10     "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
11     "monos" and
12     "print_inductives" :: diag and
13     "old_rep_datatype" :: thy_goal and
14     "primrec" :: thy_decl
15 begin
17 subsection \<open>Least fixed points\<close>
19 context complete_lattice
20 begin
22 definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
23   where "lfp f = Inf {u. f u \<le> u}"
25 lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
26   unfolding lfp_def by (rule Inf_lower) simp
28 lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
29   unfolding lfp_def by (rule Inf_greatest) simp
31 end
33 lemma lfp_fixpoint:
34   assumes "mono f"
35   shows "f (lfp f) = lfp f"
36   unfolding lfp_def
37 proof (rule order_antisym)
38   let ?H = "{u. f u \<le> u}"
39   let ?a = "\<Sqinter>?H"
40   show "f ?a \<le> ?a"
41   proof (rule Inf_greatest)
42     fix x
43     assume "x \<in> ?H"
44     then have "?a \<le> x" by (rule Inf_lower)
45     with \<open>mono f\<close> have "f ?a \<le> f x" ..
46     also from \<open>x \<in> ?H\<close> have "f x \<le> x" ..
47     finally show "f ?a \<le> x" .
48   qed
49   show "?a \<le> f ?a"
50   proof (rule Inf_lower)
51     from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
52     then show "f ?a \<in> ?H" ..
53   qed
54 qed
56 lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
57   by (rule lfp_fixpoint [symmetric])
59 lemma lfp_const: "lfp (\<lambda>x. t) = t"
60   by (rule lfp_unfold) (simp add: mono_def)
62 lemma lfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> x \<le> z) \<Longrightarrow> lfp F = x"
63   by (rule antisym) (simp_all add: lfp_lowerbound lfp_unfold[symmetric])
66 subsection \<open>General induction rules for least fixed points\<close>
68 lemma lfp_ordinal_induct [case_names mono step union]:
69   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
70   assumes mono: "mono f"
71     and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
72     and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
73   shows "P (lfp f)"
74 proof -
75   let ?M = "{S. S \<le> lfp f \<and> P S}"
76   from P_Union have "P (Sup ?M)" by simp
77   also have "Sup ?M = lfp f"
78   proof (rule antisym)
79     show "Sup ?M \<le> lfp f"
80       by (blast intro: Sup_least)
81     then have "f (Sup ?M) \<le> f (lfp f)"
82       by (rule mono [THEN monoD])
83     then have "f (Sup ?M) \<le> lfp f"
84       using mono [THEN lfp_unfold] by simp
85     then have "f (Sup ?M) \<in> ?M"
86       using P_Union by simp (intro P_f Sup_least, auto)
87     then have "f (Sup ?M) \<le> Sup ?M"
88       by (rule Sup_upper)
89     then show "lfp f \<le> Sup ?M"
90       by (rule lfp_lowerbound)
91   qed
92   finally show ?thesis .
93 qed
95 theorem lfp_induct:
96   assumes mono: "mono f"
97     and ind: "f (inf (lfp f) P) \<le> P"
98   shows "lfp f \<le> P"
99 proof (induct rule: lfp_ordinal_induct)
100   case mono
101   show ?case by fact
102 next
103   case (step S)
104   then show ?case
105     by (intro order_trans[OF _ ind] monoD[OF mono]) auto
106 next
107   case (union M)
108   then show ?case
109     by (auto intro: Sup_least)
110 qed
112 lemma lfp_induct_set:
113   assumes lfp: "a \<in> lfp f"
114     and mono: "mono f"
115     and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x"
116   shows "P a"
117   by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp)
119 lemma lfp_ordinal_induct_set:
120   assumes mono: "mono f"
121     and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
122     and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)"
123   shows "P (lfp f)"
124   using assms by (rule lfp_ordinal_induct)
127 text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
129 lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
130   by (auto intro!: lfp_unfold)
132 lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P"
133   by (blast intro: lfp_induct)
135 lemma def_lfp_induct_set:
136   "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> f (A \<inter> {x. P x}) \<Longrightarrow> P x) \<Longrightarrow> P a"
137   by (blast intro: lfp_induct_set)
139 text \<open>Monotonicity of \<open>lfp\<close>!\<close>
140 lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g"
141   by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
144 subsection \<open>Greatest fixed points\<close>
146 context complete_lattice
147 begin
149 definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
150   where "gfp f = Sup {u. u \<le> f u}"
152 lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
153   by (auto simp add: gfp_def intro: Sup_upper)
155 lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
156   by (auto simp add: gfp_def intro: Sup_least)
158 end
160 lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
161   by (rule gfp_upperbound) (simp add: lfp_fixpoint)
163 lemma gfp_fixpoint:
164   assumes "mono f"
165   shows "f (gfp f) = gfp f"
166   unfolding gfp_def
167 proof (rule order_antisym)
168   let ?H = "{u. u \<le> f u}"
169   let ?a = "\<Squnion>?H"
170   show "?a \<le> f ?a"
171   proof (rule Sup_least)
172     fix x
173     assume "x \<in> ?H"
174     then have "x \<le> f x" ..
175     also from \<open>x \<in> ?H\<close> have "x \<le> ?a" by (rule Sup_upper)
176     with \<open>mono f\<close> have "f x \<le> f ?a" ..
177     finally show "x \<le> f ?a" .
178   qed
179   show "f ?a \<le> ?a"
180   proof (rule Sup_upper)
181     from \<open>mono f\<close> and \<open>?a \<le> f ?a\<close> have "f ?a \<le> f (f ?a)" ..
182     then show "f ?a \<in> ?H" ..
183   qed
184 qed
186 lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
187   by (rule gfp_fixpoint [symmetric])
189 lemma gfp_const: "gfp (\<lambda>x. t) = t"
190   by (rule gfp_unfold) (simp add: mono_def)
192 lemma gfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> z \<le> x) \<Longrightarrow> gfp F = x"
193   by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
196 subsection \<open>Coinduction rules for greatest fixed points\<close>
198 text \<open>Weak version.\<close>
199 lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
200   by (rule gfp_upperbound [THEN subsetD]) auto
202 lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f"
203   apply (erule gfp_upperbound [THEN subsetD])
204   apply (erule imageI)
205   done
207 lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
208   apply (frule gfp_unfold [THEN eq_refl])
209   apply (drule mono_sup)
210   apply (rule le_supI)
211    apply assumption
212   apply (rule order_trans)
213    apply (rule order_trans)
214     apply assumption
215    apply (rule sup_ge2)
216   apply assumption
217   done
219 text \<open>Strong version, thanks to Coen and Frost.\<close>
220 lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f"
221   by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
223 lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
224   by (blast dest: gfp_fixpoint mono_Un)
226 lemma gfp_ordinal_induct[case_names mono step union]:
227   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
228   assumes mono: "mono f"
229     and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
230     and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
231   shows "P (gfp f)"
232 proof -
233   let ?M = "{S. gfp f \<le> S \<and> P S}"
234   from P_Union have "P (Inf ?M)" by simp
235   also have "Inf ?M = gfp f"
236   proof (rule antisym)
237     show "gfp f \<le> Inf ?M"
238       by (blast intro: Inf_greatest)
239     then have "f (gfp f) \<le> f (Inf ?M)"
240       by (rule mono [THEN monoD])
241     then have "gfp f \<le> f (Inf ?M)"
242       using mono [THEN gfp_unfold] by simp
243     then have "f (Inf ?M) \<in> ?M"
244       using P_Union by simp (intro P_f Inf_greatest, auto)
245     then have "Inf ?M \<le> f (Inf ?M)"
246       by (rule Inf_lower)
247     then show "Inf ?M \<le> gfp f"
248       by (rule gfp_upperbound)
249   qed
250   finally show ?thesis .
251 qed
253 lemma coinduct:
254   assumes mono: "mono f"
255     and ind: "X \<le> f (sup X (gfp f))"
256   shows "X \<le> gfp f"
257 proof (induct rule: gfp_ordinal_induct)
258   case mono
259   then show ?case by fact
260 next
261   case (step S)
262   then show ?case
263     by (intro order_trans[OF ind _] monoD[OF mono]) auto
264 next
265   case (union M)
266   then show ?case
267     by (auto intro: mono Inf_greatest)
268 qed
271 subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
273 text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
274   @{term lfp} and @{term gfp}\<close>
275 lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
276   by (iprover intro: subset_refl monoI Un_mono monoD)
278 lemma coinduct3_lemma:
279   "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
280     lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
281   apply (rule subset_trans)
282    apply (erule coinduct3_mono_lemma [THEN lfp_unfold [THEN eq_refl]])
283   apply (rule Un_least [THEN Un_least])
284     apply (rule subset_refl, assumption)
285   apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
286   apply (rule monoD, assumption)
287   apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
288   done
290 lemma coinduct3: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> a \<in> gfp f"
291   apply (rule coinduct3_lemma [THEN  weak_coinduct])
292     apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
293      apply simp_all
294   done
296 text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
298 lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
299   by (auto intro!: gfp_unfold)
301 lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A"
302   by (iprover intro!: coinduct)
304 lemma def_coinduct_set: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> A) \<Longrightarrow> a \<in> A"
305   by (auto intro!: coinduct_set)
307 lemma def_Collect_coinduct:
308   "A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow>
309     (\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A"
310   by (erule def_coinduct_set) auto
312 lemma def_coinduct3: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> A)) \<Longrightarrow> a \<in> A"
313   by (auto intro!: coinduct3)
315 text \<open>Monotonicity of @{term gfp}!\<close>
316 lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
317   by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
320 subsection \<open>Rules for fixed point calculus\<close>
322 lemma lfp_rolling:
323   assumes "mono g" "mono f"
324   shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
325 proof (rule antisym)
326   have *: "mono (\<lambda>x. f (g x))"
327     using assms by (auto simp: mono_def)
328   show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
329     by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
330   show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
331   proof (rule lfp_greatest)
332     fix u
333     assume u: "g (f u) \<le> u"
334     then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
335       by (intro assms[THEN monoD] lfp_lowerbound)
336     with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
337       by auto
338   qed
339 qed
341 lemma lfp_lfp:
342   assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
343   shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
344 proof (rule antisym)
345   have *: "mono (\<lambda>x. f x x)"
346     by (blast intro: monoI f)
347   show "lfp (\<lambda>x. lfp (f x)) \<le> lfp (\<lambda>x. f x x)"
348     by (intro lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
349   show "lfp (\<lambda>x. lfp (f x)) \<ge> lfp (\<lambda>x. f x x)" (is "?F \<ge> _")
350   proof (intro lfp_lowerbound)
351     have *: "?F = lfp (f ?F)"
352       by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
353     also have "\<dots> = f ?F (lfp (f ?F))"
354       by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
355     finally show "f ?F ?F \<le> ?F"
356       by (simp add: *[symmetric])
357   qed
358 qed
360 lemma gfp_rolling:
361   assumes "mono g" "mono f"
362   shows "g (gfp (\<lambda>x. f (g x))) = gfp (\<lambda>x. g (f x))"
363 proof (rule antisym)
364   have *: "mono (\<lambda>x. f (g x))"
365     using assms by (auto simp: mono_def)
366   show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
367     by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
368   show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
369   proof (rule gfp_least)
370     fix u
371     assume u: "u \<le> g (f u)"
372     then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
373       by (intro assms[THEN monoD] gfp_upperbound)
374     with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
375       by auto
376   qed
377 qed
379 lemma gfp_gfp:
380   assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
381   shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"
382 proof (rule antisym)
383   have *: "mono (\<lambda>x. f x x)"
384     by (blast intro: monoI f)
385   show "gfp (\<lambda>x. f x x) \<le> gfp (\<lambda>x. gfp (f x))"
386     by (intro gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
387   show "gfp (\<lambda>x. gfp (f x)) \<le> gfp (\<lambda>x. f x x)" (is "?F \<le> _")
388   proof (intro gfp_upperbound)
389     have *: "?F = gfp (f ?F)"
390       by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
391     also have "\<dots> = f ?F (gfp (f ?F))"
392       by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
393     finally show "?F \<le> f ?F ?F"
394       by (simp add: *[symmetric])
395   qed
396 qed
399 subsection \<open>Inductive predicates and sets\<close>
401 text \<open>Package setup.\<close>
403 lemmas basic_monos =
404   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
405   Collect_mono in_mono vimage_mono
407 lemma le_rel_bool_arg_iff: "X \<le> Y \<longleftrightarrow> X False \<le> Y False \<and> X True \<le> Y True"
408   unfolding le_fun_def le_bool_def using bool_induct by auto
410 lemma imp_conj_iff: "((P \<longrightarrow> Q) \<and> P) = (P \<and> Q)"
411   by blast
413 lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
414   by auto
416 ML_file "Tools/inductive.ML"
418 lemmas [mono] =
419   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
420   imp_mono not_mono
421   Ball_def Bex_def
422   induct_rulify_fallback
425 subsection \<open>The Schroeder-Bernstein Theorem\<close>
427 text \<open>
429   \<^item> \<^file>\<open>\$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close>
430   \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close>
431   \<^item> Springer LNCS 828 (cover page)
432 \<close>
434 theorem Schroeder_Bernstein:
435   fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a"
436     and A :: "'a set" and B :: "'b set"
437   assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B"
438     and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A"
439   shows "\<exists>h. bij_betw h A B"
440 proof (rule exI, rule bij_betw_imageI)
441   define X where "X = lfp (\<lambda>X. A - (g ` (B - (f ` X))))"
442   define g' where "g' = the_inv_into (B - (f ` X)) g"
443   let ?h = "\<lambda>z. if z \<in> X then f z else g' z"
445   have X: "X = A - (g ` (B - (f ` X)))"
446     unfolding X_def by (rule lfp_unfold) (blast intro: monoI)
447   then have X_compl: "A - X = g ` (B - (f ` X))"
448     using sub2 by blast
450   from inj2 have inj2': "inj_on g (B - (f ` X))"
451     by (rule inj_on_subset) auto
452   with X_compl have *: "g' ` (A - X) = B - (f ` X)"
453     by (simp add: g'_def)
455   from X have X_sub: "X \<subseteq> A" by auto
456   from X sub1 have fX_sub: "f ` X \<subseteq> B" by auto
458   show "?h ` A = B"
459   proof -
460     from X_sub have "?h ` A = ?h ` (X \<union> (A - X))" by auto
461     also have "\<dots> = ?h ` X \<union> ?h ` (A - X)" by (simp only: image_Un)
462     also have "?h ` X = f ` X" by auto
463     also from * have "?h ` (A - X) = B - (f ` X)" by auto
464     also from fX_sub have "f ` X \<union> (B - f ` X) = B" by blast
465     finally show ?thesis .
466   qed
467   show "inj_on ?h A"
468   proof -
469     from inj1 X_sub have on_X: "inj_on f X"
470       by (rule subset_inj_on)
472     have on_X_compl: "inj_on g' (A - X)"
473       unfolding g'_def X_compl
474       by (rule inj_on_the_inv_into) (rule inj2')
476     have impossible: False if eq: "f a = g' b" and a: "a \<in> X" and b: "b \<in> A - X" for a b
477     proof -
478       from a have fa: "f a \<in> f ` X" by (rule imageI)
479       from b have "g' b \<in> g' ` (A - X)" by (rule imageI)
480       with * have "g' b \<in> - (f ` X)" by simp
481       with eq fa show False by simp
482     qed
484     show ?thesis
485     proof (rule inj_onI)
486       fix a b
487       assume h: "?h a = ?h b"
488       assume "a \<in> A" and "b \<in> A"
489       then consider "a \<in> X" "b \<in> X" | "a \<in> A - X" "b \<in> A - X"
490         | "a \<in> X" "b \<in> A - X" | "a \<in> A - X" "b \<in> X"
491         by blast
492       then show "a = b"
493       proof cases
494         case 1
495         with h on_X show ?thesis by (simp add: inj_on_eq_iff)
496       next
497         case 2
498         with h on_X_compl show ?thesis by (simp add: inj_on_eq_iff)
499       next
500         case 3
501         with h impossible [of a b] have False by simp
502         then show ?thesis ..
503       next
504         case 4
505         with h impossible [of b a] have False by simp
506         then show ?thesis ..
507       qed
508     qed
509   qed
510 qed
513 subsection \<open>Inductive datatypes and primitive recursion\<close>
515 text \<open>Package setup.\<close>
517 ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
518 ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
519 ML_file "Tools/Old_Datatype/old_datatype_data.ML"
520 ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
521 ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
522 ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
523 ML_file "Tools/Old_Datatype/old_primrec.ML"
524 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
526 text \<open>Lambda-abstractions with pattern matching:\<close>
527 syntax (ASCII)
528   "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
529 syntax
530   "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
531 parse_translation \<open>
532   let
533     fun fun_tr ctxt [cs] =
534       let
535         val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
536         val ft = Case_Translation.case_tr true ctxt [x, cs];
537       in lambda x ft end
538   in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
539 \<close>
541 end