src/HOL/Inductive.thy
 changeset 63980 f8e556c8ad6f parent 63979 95c3ae4baba8 child 63981 6f7db4f8df4c
```     1.1 --- a/src/HOL/Inductive.thy	Sat Oct 01 17:16:35 2016 +0200
1.2 +++ b/src/HOL/Inductive.thy	Sat Oct 01 17:38:14 2016 +0200
1.3 @@ -422,6 +422,94 @@
1.4    induct_rulify_fallback
1.5
1.6
1.7 +subsection \<open>The Schroeder-Bernstein Theorem\<close>
1.8 +
1.9 +text \<open>
1.11 +  \<^item> \<^file>\<open>\$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close>
1.12 +  \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close>
1.13 +  \<^item> Springer LNCS 828 (cover page)
1.14 +\<close>
1.15 +
1.16 +theorem Schroeder_Bernstein:
1.17 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a"
1.18 +    and A :: "'a set" and B :: "'b set"
1.19 +  assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B"
1.20 +    and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A"
1.21 +  shows "\<exists>h. bij_betw h A B"
1.22 +proof (rule exI, rule bij_betw_imageI)
1.23 +  define X where "X = lfp (\<lambda>X. A - (g ` (B - (f ` X))))"
1.24 +  define g' where "g' = the_inv_into (B - (f ` X)) g"
1.25 +  let ?h = "\<lambda>z. if z \<in> X then f z else g' z"
1.26 +
1.27 +  have X: "X = A - (g ` (B - (f ` X)))"
1.28 +    unfolding X_def by (rule lfp_unfold) (blast intro: monoI)
1.29 +  then have X_compl: "A - X = g ` (B - (f ` X))"
1.30 +    using sub2 by blast
1.31 +
1.32 +  from inj2 have inj2': "inj_on g (B - (f ` X))"
1.33 +    by (rule inj_on_subset) auto
1.34 +  with X_compl have *: "g' ` (A - X) = B - (f ` X)"
1.35 +    by (simp add: g'_def)
1.36 +
1.37 +  from X have X_sub: "X \<subseteq> A" by auto
1.38 +  from X sub1 have fX_sub: "f ` X \<subseteq> B" by auto
1.39 +
1.40 +  show "?h ` A = B"
1.41 +  proof -
1.42 +    from X_sub have "?h ` A = ?h ` (X \<union> (A - X))" by auto
1.43 +    also have "\<dots> = ?h ` X \<union> ?h ` (A - X)" by (simp only: image_Un)
1.44 +    also have "?h ` X = f ` X" by auto
1.45 +    also from * have "?h ` (A - X) = B - (f ` X)" by auto
1.46 +    also from fX_sub have "f ` X \<union> (B - f ` X) = B" by blast
1.47 +    finally show ?thesis .
1.48 +  qed
1.49 +  show "inj_on ?h A"
1.50 +  proof -
1.51 +    from inj1 X_sub have on_X: "inj_on f X"
1.52 +      by (rule subset_inj_on)
1.53 +
1.54 +    have on_X_compl: "inj_on g' (A - X)"
1.55 +      unfolding g'_def X_compl
1.56 +      by (rule inj_on_the_inv_into) (rule inj2')
1.57 +
1.58 +    have impossible: False if eq: "f a = g' b" and a: "a \<in> X" and b: "b \<in> A - X" for a b
1.59 +    proof -
1.60 +      from a have fa: "f a \<in> f ` X" by (rule imageI)
1.61 +      from b have "g' b \<in> g' ` (A - X)" by (rule imageI)
1.62 +      with * have "g' b \<in> - (f ` X)" by simp
1.63 +      with eq fa show False by simp
1.64 +    qed
1.65 +
1.66 +    show ?thesis
1.67 +    proof (rule inj_onI)
1.68 +      fix a b
1.69 +      assume h: "?h a = ?h b"
1.70 +      assume "a \<in> A" and "b \<in> A"
1.71 +      then consider "a \<in> X" "b \<in> X" | "a \<in> A - X" "b \<in> A - X"
1.72 +        | "a \<in> X" "b \<in> A - X" | "a \<in> A - X" "b \<in> X"
1.73 +        by blast
1.74 +      then show "a = b"
1.75 +      proof cases
1.76 +        case 1
1.77 +        with h on_X show ?thesis by (simp add: inj_on_eq_iff)
1.78 +      next
1.79 +        case 2
1.80 +        with h on_X_compl show ?thesis by (simp add: inj_on_eq_iff)
1.81 +      next
1.82 +        case 3
1.83 +        with h impossible [of a b] have False by simp
1.84 +        then show ?thesis ..
1.85 +      next
1.86 +        case 4
1.87 +        with h impossible [of b a] have False by simp
1.88 +        then show ?thesis ..
1.89 +      qed
1.90 +    qed
1.91 +  qed
1.92 +qed
1.93 +
1.94 +
1.95  subsection \<open>Inductive datatypes and primitive recursion\<close>
1.96
1.97  text \<open>Package setup.\<close>
```