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