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.10 +  See also:
    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>