1(*  Title:      HOL/Inductive.thy
2    Author:     Markus Wenzel, TU Muenchen
3*)
4
5section \<open>Knaster-Tarski Fixpoint Theorem and inductive definitions\<close>
6
7theory 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
15begin
16
17subsection \<open>Least fixed points\<close>
18
19context complete_lattice
20begin
21
22definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
23  where "lfp f = Inf {u. f u \<le> u}"
24
25lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
26  unfolding lfp_def by (rule Inf_lower) simp
27
28lemma 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
30
31end
32
33lemma lfp_fixpoint:
34  assumes "mono f"
35  shows "f (lfp f) = lfp f"
36  unfolding lfp_def
37proof (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
54qed
55
56lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
57  by (rule lfp_fixpoint [symmetric])
58
59lemma lfp_const: "lfp (\<lambda>x. t) = t"
60  by (rule lfp_unfold) (simp add: mono_def)
61
62lemma 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])
64
65
66subsection \<open>General induction rules for least fixed points\<close>
67
68lemma 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)"
74proof -
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 .
93qed
94
95theorem lfp_induct:
96  assumes mono: "mono f"
97    and ind: "f (inf (lfp f) P) \<le> P"
98  shows "lfp f \<le> P"
99proof (induct rule: lfp_ordinal_induct)
100  case mono
101  show ?case by fact
102next
103  case (step S)
104  then show ?case
105    by (intro order_trans[OF _ ind] monoD[OF mono]) auto
106next
107  case (union M)
108  then show ?case
109    by (auto intro: Sup_least)
110qed
111
112lemma 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)
118
119lemma 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)
125
126
127text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
128
129lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
130  by (auto intro!: lfp_unfold)
131
132lemma 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)
134
135lemma 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)
138
139text \<open>Monotonicity of \<open>lfp\<close>!\<close>
140lemma 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)
142
143
144subsection \<open>Greatest fixed points\<close>
145
146context complete_lattice
147begin
148
149definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
150  where "gfp f = Sup {u. u \<le> f u}"
151
152lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
153  by (auto simp add: gfp_def intro: Sup_upper)
154
155lemma 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)
157
158end
159
160lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
161  by (rule gfp_upperbound) (simp add: lfp_fixpoint)
162
163lemma gfp_fixpoint:
164  assumes "mono f"
165  shows "f (gfp f) = gfp f"
166  unfolding gfp_def
167proof (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
184qed
185
186lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
187  by (rule gfp_fixpoint [symmetric])
188
189lemma gfp_const: "gfp (\<lambda>x. t) = t"
190  by (rule gfp_unfold) (simp add: mono_def)
191
192lemma 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])
194
195
196subsection \<open>Coinduction rules for greatest fixed points\<close>
197
198text \<open>Weak version.\<close>
199lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
200  by (rule gfp_upperbound [THEN subsetD]) auto
201
202lemma 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
206
207lemma 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
218
219text \<open>Strong version, thanks to Coen and Frost.\<close>
220lemma 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+
222
223lemma 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)
225
226lemma 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)"
232proof -
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 .
251qed
252
253lemma coinduct:
254  assumes mono: "mono f"
255    and ind: "X \<le> f (sup X (gfp f))"
256  shows "X \<le> gfp f"
257proof (induct rule: gfp_ordinal_induct)
258  case mono
259  then show ?case by fact
260next
261  case (step S)
262  then show ?case
263    by (intro order_trans[OF ind _] monoD[OF mono]) auto
264next
265  case (union M)
266  then show ?case
267    by (auto intro: mono Inf_greatest)
268qed
269
270
271subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
272
273text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
274  @{term lfp} and @{term gfp}\<close>
275lemma 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)
277
278lemma 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
289
290lemma 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 [2] weak_coinduct])
292    apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
293     apply simp_all
294  done
295
296text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
297
298lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
299  by (auto intro!: gfp_unfold)
300
301lemma 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)
303
304lemma 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)
306
307lemma 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
311
312lemma 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)
314
315text \<open>Monotonicity of @{term gfp}!\<close>
316lemma 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)
318
319
320subsection \<open>Rules for fixed point calculus\<close>
321
322lemma lfp_rolling:
323  assumes "mono g" "mono f"
324  shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
325proof (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
339qed
340
341lemma 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)"
344proof (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
358qed
359
360lemma gfp_rolling:
361  assumes "mono g" "mono f"
362  shows "g (gfp (\<lambda>x. f (g x))) = gfp (\<lambda>x. g (f x))"
363proof (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
377qed
378
379lemma 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)"
382proof (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
396qed
397
398
399subsection \<open>Inductive predicates and sets\<close>
400
401text \<open>Package setup.\<close>
402
403lemmas 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
406
407lemma 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
409
410lemma imp_conj_iff: "((P \<longrightarrow> Q) \<and> P) = (P \<and> Q)"
411  by blast
412
413lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
414  by auto
415
416ML_file "Tools/inductive.ML"
417
418lemmas [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
423
424
425subsection \<open>The Schroeder-Bernstein Theorem\<close>
426
427text \<open>
428  See also:
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>
433
434theorem 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"
440proof (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"
444
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
449
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)
454
455  from X have X_sub: "X \<subseteq> A" by auto
456  from X sub1 have fX_sub: "f ` X \<subseteq> B" by auto
457
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)
471
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')
475
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
483
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
510qed
511
512
513subsection \<open>Inductive datatypes and primitive recursion\<close>
514
515text \<open>Package setup.\<close>
516
517ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
518ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
519ML_file "Tools/Old_Datatype/old_datatype_data.ML"
520ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
521ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
522ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
523ML_file "Tools/Old_Datatype/old_primrec.ML"
524ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
525
526text \<open>Lambda-abstractions with pattern matching:\<close>
527syntax (ASCII)
528  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
529syntax
530  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
531parse_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>
540
541end
542