src/HOL/Inductive.thy
author wenzelm
Thu Mar 14 16:55:06 2019 +0100 (5 weeks ago)
changeset 69913 ca515cf61651
parent 69605 a96320074298
permissions -rw-r--r--
more specific keyword kinds;
     1 (*  Title:      HOL/Inductive.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 section \<open>Knaster-Tarski Fixpoint Theorem and inductive definitions\<close>
     6 
     7 theory Inductive
     8   imports Complete_Lattices Ctr_Sugar
     9   keywords
    10     "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_defn and
    11     "monos" and
    12     "print_inductives" :: diag and
    13     "old_rep_datatype" :: thy_goal and
    14     "primrec" :: thy_defn
    15 begin
    16 
    17 subsection \<open>Least fixed points\<close>
    18 
    19 context complete_lattice
    20 begin
    21 
    22 definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
    23   where "lfp f = Inf {u. f u \<le> u}"
    24 
    25 lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
    26   unfolding lfp_def by (rule Inf_lower) simp
    27 
    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
    30 
    31 end
    32 
    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
    55 
    56 lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
    57   by (rule lfp_fixpoint [symmetric])
    58 
    59 lemma lfp_const: "lfp (\<lambda>x. t) = t"
    60   by (rule lfp_unfold) (simp add: mono_def)
    61 
    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])
    64 
    65 
    66 subsection \<open>General induction rules for least fixed points\<close>
    67 
    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
    94 
    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
   111 
   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)
   118 
   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)
   125 
   126 
   127 text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
   128 
   129 lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
   130   by (auto intro!: lfp_unfold)
   131 
   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)
   134 
   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)
   138 
   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)
   142 
   143 
   144 subsection \<open>Greatest fixed points\<close>
   145 
   146 context complete_lattice
   147 begin
   148 
   149 definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
   150   where "gfp f = Sup {u. u \<le> f u}"
   151 
   152 lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
   153   by (auto simp add: gfp_def intro: Sup_upper)
   154 
   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)
   157 
   158 end
   159 
   160 lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
   161   by (rule gfp_upperbound) (simp add: lfp_fixpoint)
   162 
   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
   185 
   186 lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   187   by (rule gfp_fixpoint [symmetric])
   188 
   189 lemma gfp_const: "gfp (\<lambda>x. t) = t"
   190   by (rule gfp_unfold) (simp add: mono_def)
   191 
   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])
   194 
   195 
   196 subsection \<open>Coinduction rules for greatest fixed points\<close>
   197 
   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
   201 
   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
   206 
   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
   218 
   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+
   222 
   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)
   225 
   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
   252 
   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
   269 
   270 
   271 subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
   272 
   273 text \<open>Weakens the condition \<^term>\<open>X \<subseteq> f X\<close> to one expressed using both
   274   \<^term>\<open>lfp\<close> and \<^term>\<open>gfp\<close>\<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)
   277 
   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
   289 
   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 [2] weak_coinduct])
   292     apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
   293      apply simp_all
   294   done
   295 
   296 text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
   297 
   298 lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
   299   by (auto intro!: gfp_unfold)
   300 
   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)
   303 
   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)
   306 
   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
   311 
   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)
   314 
   315 text \<open>Monotonicity of \<^term>\<open>gfp\<close>!\<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)
   318 
   319 
   320 subsection \<open>Rules for fixed point calculus\<close>
   321 
   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
   340 
   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
   359 
   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
   378 
   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
   397 
   398 
   399 subsection \<open>Inductive predicates and sets\<close>
   400 
   401 text \<open>Package setup.\<close>
   402 
   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
   406 
   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
   409 
   410 lemma imp_conj_iff: "((P \<longrightarrow> Q) \<and> P) = (P \<and> Q)"
   411   by blast
   412 
   413 lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
   414   by auto
   415 
   416 ML_file \<open>Tools/inductive.ML\<close>
   417 
   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
   423 
   424 
   425 subsection \<open>The Schroeder-Bernstein Theorem\<close>
   426 
   427 text \<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 
   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"
   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
   510 qed
   511 
   512 
   513 subsection \<open>Inductive datatypes and primitive recursion\<close>
   514 
   515 text \<open>Package setup.\<close>
   516 
   517 ML_file \<open>Tools/Old_Datatype/old_datatype_aux.ML\<close>
   518 ML_file \<open>Tools/Old_Datatype/old_datatype_prop.ML\<close>
   519 ML_file \<open>Tools/Old_Datatype/old_datatype_data.ML\<close>
   520 ML_file \<open>Tools/Old_Datatype/old_rep_datatype.ML\<close>
   521 ML_file \<open>Tools/Old_Datatype/old_datatype_codegen.ML\<close>
   522 ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_util.ML\<close>
   523 ML_file \<open>Tools/Old_Datatype/old_primrec.ML\<close>
   524 ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar.ML\<close>
   525 
   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>\<open>_lam_pats_syntax\<close>, fun_tr)] end
   539 \<close>
   540 
   541 end