Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
authorwenzelm
Sat Oct 01 17:38:14 2016 +0200 (2016-10-01)
changeset 63980f8e556c8ad6f
parent 63979 95c3ae4baba8
child 63981 6f7db4f8df4c
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Inductive.thy
src/HOL/Isar_Examples/Schroeder_Bernstein.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sat Oct 01 17:16:35 2016 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sat Oct 01 17:38:14 2016 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4     card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
     1.5     embed_Field[of "|B|" "|A|" g] by auto
     1.6     obtain h where "bij_betw h A B"
     1.7 -   using * ** 1 Cantor_Bernstein[of f] by fastforce
     1.8 +   using * ** 1 Schroeder_Bernstein[of f] by fastforce
     1.9     hence "|A| =o |B|" using card_of_ordIso by blast
    1.10     hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto
    1.11    }
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Oct 01 17:16:35 2016 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Oct 01 17:38:14 2016 +0200
     2.3 @@ -450,106 +450,6 @@
     2.4    using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
     2.5  
     2.6  
     2.7 -subsection \<open>The Cantor-Bernstein Theorem\<close>
     2.8 -
     2.9 -lemma Cantor_Bernstein_aux:
    2.10 -  "\<exists>A' h. A' \<subseteq> A \<and>
    2.11 -    (\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')) \<and>
    2.12 -    (\<forall>a \<in> A'. h a = f a) \<and>
    2.13 -    (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a))"
    2.14 -proof -
    2.15 -  define H where "H A' = A - (g ` (B - (f ` A')))" for A'
    2.16 -  have "mono H" unfolding mono_def H_def by blast
    2.17 -  from lfp_unfold [OF this] obtain A' where "H A' = A'" by blast
    2.18 -  then have "A' = A - (g ` (B - (f ` A')))" by (simp add: H_def)
    2.19 -  then have 1: "A' \<subseteq> A"
    2.20 -    and 2: "\<forall>a \<in> A'.  a \<notin> g ` (B - f ` A')"
    2.21 -    and 3: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
    2.22 -    by blast+
    2.23 -  define h where "h a = (if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" for a
    2.24 -  then have 4: "\<forall>a \<in> A'. h a = f a" by simp
    2.25 -  have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)"
    2.26 -  proof
    2.27 -    fix a
    2.28 -    let ?phi = "\<lambda>b. b \<in> B - (f ` A') \<and> a = g b"
    2.29 -    assume *: "a \<in> A - A'"
    2.30 -    from * have "h a = (SOME b. ?phi b)" by (auto simp: h_def)
    2.31 -    moreover from 3 * have "\<exists>b. ?phi b" by auto
    2.32 -    ultimately show "?phi (h a)"
    2.33 -      using someI_ex[of ?phi] by auto
    2.34 -  qed
    2.35 -  with 1 2 4 show ?thesis by blast
    2.36 -qed
    2.37 -
    2.38 -theorem Cantor_Bernstein:
    2.39 -  assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B"
    2.40 -    and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A"
    2.41 -  shows "\<exists>h. bij_betw h A B"
    2.42 -proof-
    2.43 -  obtain A' and h where "A' \<subseteq> A"
    2.44 -    and 1: "\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')"
    2.45 -    and 2: "\<forall>a \<in> A'. h a = f a"
    2.46 -    and 3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)"
    2.47 -    using Cantor_Bernstein_aux [of A g B f] by blast
    2.48 -  have "inj_on h A"
    2.49 -  proof (intro inj_onI)
    2.50 -    fix a1 a2
    2.51 -    assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2"
    2.52 -    show "a1 = a2"
    2.53 -    proof (cases "a1 \<in> A'")
    2.54 -      case True
    2.55 -      show ?thesis
    2.56 -      proof (cases "a2 \<in> A'")
    2.57 -        case True': True
    2.58 -        with True 2 6 have "f a1 = f a2" by auto
    2.59 -        with inj1 \<open>A' \<subseteq> A\<close> True True' show ?thesis
    2.60 -          unfolding inj_on_def by blast
    2.61 -      next
    2.62 -        case False
    2.63 -        with 2 3 5 6 True have False by force
    2.64 -        then show ?thesis ..
    2.65 -      qed
    2.66 -    next
    2.67 -      case False
    2.68 -      show ?thesis
    2.69 -      proof (cases "a2 \<in> A'")
    2.70 -        case True
    2.71 -        with 2 3 4 6 False have False by auto
    2.72 -        then show ?thesis ..
    2.73 -      next
    2.74 -        case False': False
    2.75 -        with False 3 4 5 have "a1 = g (h a1)" "a2 = g (h a2)" by auto
    2.76 -        with 6 show ?thesis by simp
    2.77 -      qed
    2.78 -    qed
    2.79 -  qed
    2.80 -  moreover have "h ` A = B"
    2.81 -  proof safe
    2.82 -    fix a
    2.83 -    assume "a \<in> A"
    2.84 -    with sub1 2 3 show "h a \<in> B" by (cases "a \<in> A'") auto
    2.85 -  next
    2.86 -    fix b
    2.87 -    assume *: "b \<in> B"
    2.88 -    show "b \<in> h ` A"
    2.89 -    proof (cases "b \<in> f ` A'")
    2.90 -      case True
    2.91 -      then obtain a where "a \<in> A'" "b = f a" by blast
    2.92 -      with \<open>A' \<subseteq> A\<close> 2 show ?thesis by force
    2.93 -    next
    2.94 -      case False
    2.95 -      with 1 * have "g b \<notin> A'" by auto
    2.96 -      with sub2 * have 4: "g b \<in> A - A'" by auto
    2.97 -      with 3 have "h (g b) \<in> B" "g (h (g b)) = g b" by auto
    2.98 -      with inj2 * have "h (g b) = b" by (auto simp: inj_on_def)
    2.99 -      with 4 show ?thesis by force
   2.100 -    qed
   2.101 -  qed
   2.102 -  ultimately show ?thesis
   2.103 -    by (auto simp: bij_betw_def)
   2.104 -qed
   2.105 -
   2.106 -
   2.107  subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
   2.108  
   2.109  text \<open>Hilbert's Epsilon and the @{term split} Operator\<close>
     3.1 --- a/src/HOL/Inductive.thy	Sat Oct 01 17:16:35 2016 +0200
     3.2 +++ b/src/HOL/Inductive.thy	Sat Oct 01 17:38:14 2016 +0200
     3.3 @@ -422,6 +422,94 @@
     3.4    induct_rulify_fallback
     3.5  
     3.6  
     3.7 +subsection \<open>The Schroeder-Bernstein Theorem\<close>
     3.8 +
     3.9 +text \<open>
    3.10 +  See also:
    3.11 +  \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close>
    3.12 +  \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close>
    3.13 +  \<^item> Springer LNCS 828 (cover page)
    3.14 +\<close>
    3.15 +
    3.16 +theorem Schroeder_Bernstein:
    3.17 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a"
    3.18 +    and A :: "'a set" and B :: "'b set"
    3.19 +  assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B"
    3.20 +    and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A"
    3.21 +  shows "\<exists>h. bij_betw h A B"
    3.22 +proof (rule exI, rule bij_betw_imageI)
    3.23 +  define X where "X = lfp (\<lambda>X. A - (g ` (B - (f ` X))))"
    3.24 +  define g' where "g' = the_inv_into (B - (f ` X)) g"
    3.25 +  let ?h = "\<lambda>z. if z \<in> X then f z else g' z"
    3.26 +
    3.27 +  have X: "X = A - (g ` (B - (f ` X)))"
    3.28 +    unfolding X_def by (rule lfp_unfold) (blast intro: monoI)
    3.29 +  then have X_compl: "A - X = g ` (B - (f ` X))"
    3.30 +    using sub2 by blast
    3.31 +
    3.32 +  from inj2 have inj2': "inj_on g (B - (f ` X))"
    3.33 +    by (rule inj_on_subset) auto
    3.34 +  with X_compl have *: "g' ` (A - X) = B - (f ` X)"
    3.35 +    by (simp add: g'_def)
    3.36 +
    3.37 +  from X have X_sub: "X \<subseteq> A" by auto
    3.38 +  from X sub1 have fX_sub: "f ` X \<subseteq> B" by auto
    3.39 +
    3.40 +  show "?h ` A = B"
    3.41 +  proof -
    3.42 +    from X_sub have "?h ` A = ?h ` (X \<union> (A - X))" by auto
    3.43 +    also have "\<dots> = ?h ` X \<union> ?h ` (A - X)" by (simp only: image_Un)
    3.44 +    also have "?h ` X = f ` X" by auto
    3.45 +    also from * have "?h ` (A - X) = B - (f ` X)" by auto
    3.46 +    also from fX_sub have "f ` X \<union> (B - f ` X) = B" by blast
    3.47 +    finally show ?thesis .
    3.48 +  qed
    3.49 +  show "inj_on ?h A"
    3.50 +  proof -
    3.51 +    from inj1 X_sub have on_X: "inj_on f X"
    3.52 +      by (rule subset_inj_on)
    3.53 +
    3.54 +    have on_X_compl: "inj_on g' (A - X)"
    3.55 +      unfolding g'_def X_compl
    3.56 +      by (rule inj_on_the_inv_into) (rule inj2')
    3.57 +
    3.58 +    have impossible: False if eq: "f a = g' b" and a: "a \<in> X" and b: "b \<in> A - X" for a b
    3.59 +    proof -
    3.60 +      from a have fa: "f a \<in> f ` X" by (rule imageI)
    3.61 +      from b have "g' b \<in> g' ` (A - X)" by (rule imageI)
    3.62 +      with * have "g' b \<in> - (f ` X)" by simp
    3.63 +      with eq fa show False by simp
    3.64 +    qed
    3.65 +
    3.66 +    show ?thesis
    3.67 +    proof (rule inj_onI)
    3.68 +      fix a b
    3.69 +      assume h: "?h a = ?h b"
    3.70 +      assume "a \<in> A" and "b \<in> A"
    3.71 +      then consider "a \<in> X" "b \<in> X" | "a \<in> A - X" "b \<in> A - X"
    3.72 +        | "a \<in> X" "b \<in> A - X" | "a \<in> A - X" "b \<in> X"
    3.73 +        by blast
    3.74 +      then show "a = b"
    3.75 +      proof cases
    3.76 +        case 1
    3.77 +        with h on_X show ?thesis by (simp add: inj_on_eq_iff)
    3.78 +      next
    3.79 +        case 2
    3.80 +        with h on_X_compl show ?thesis by (simp add: inj_on_eq_iff)
    3.81 +      next
    3.82 +        case 3
    3.83 +        with h impossible [of a b] have False by simp
    3.84 +        then show ?thesis ..
    3.85 +      next
    3.86 +        case 4
    3.87 +        with h impossible [of b a] have False by simp
    3.88 +        then show ?thesis ..
    3.89 +      qed
    3.90 +    qed
    3.91 +  qed
    3.92 +qed
    3.93 +
    3.94 +
    3.95  subsection \<open>Inductive datatypes and primitive recursion\<close>
    3.96  
    3.97  text \<open>Package setup.\<close>
     4.1 --- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Sat Oct 01 17:16:35 2016 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,56 +0,0 @@
     4.4 -(*  Title:      HOL/Isar_Examples/Schroeder_Bernstein.thy
     4.5 -    Author:     Makarius
     4.6 -*)
     4.7 -
     4.8 -section \<open>Schröder-Bernstein Theorem\<close>
     4.9 -
    4.10 -theory Schroeder_Bernstein
    4.11 -  imports Main
    4.12 -begin
    4.13 -
    4.14 -text \<open>
    4.15 -  See also:
    4.16 -  \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close>
    4.17 -  \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close>
    4.18 -  \<^item> Springer LNCS 828 (cover page)
    4.19 -\<close>
    4.20 -
    4.21 -theorem Schroeder_Bernstein: \<open>\<exists>h :: 'a \<Rightarrow> 'b. inj h \<and> surj h\<close> if \<open>inj f\<close> and \<open>inj g\<close>
    4.22 -  for f :: \<open>'a \<Rightarrow> 'b\<close> and g :: \<open>'b \<Rightarrow> 'a\<close>
    4.23 -proof
    4.24 -  define A where \<open>A = lfp (\<lambda>X. - (g ` (- (f ` X))))\<close>
    4.25 -  define g' where \<open>g' = inv g\<close>
    4.26 -  let \<open>?h\<close> = \<open>\<lambda>z. if z \<in> A then f z else g' z\<close>
    4.27 -
    4.28 -  have \<open>A = - (g ` (- (f ` A)))\<close>
    4.29 -    unfolding A_def by (rule lfp_unfold) (blast intro: monoI)
    4.30 -  then have A_compl: \<open>- A = g ` (- (f ` A))\<close> by blast
    4.31 -  then have *: \<open>g' ` (- A) = - (f ` A)\<close>
    4.32 -    using g'_def \<open>inj g\<close> by auto
    4.33 -
    4.34 -  show \<open>inj ?h \<and> surj ?h\<close>
    4.35 -  proof
    4.36 -    from * show \<open>surj ?h\<close> by auto
    4.37 -    have \<open>inj_on f A\<close>
    4.38 -      using \<open>inj f\<close> by (rule subset_inj_on) blast
    4.39 -    moreover
    4.40 -    have \<open>inj_on g' (- A)\<close>
    4.41 -      unfolding g'_def
    4.42 -    proof (rule inj_on_inv_into)
    4.43 -      have \<open>g ` (- (f ` A)) \<subseteq> range g\<close> by blast
    4.44 -      then show \<open>- A \<subseteq> range g\<close> by (simp only: A_compl)
    4.45 -    qed
    4.46 -    moreover
    4.47 -    have \<open>False\<close> if eq: \<open>f a = g' b\<close> and a: \<open>a \<in> A\<close> and b: \<open>b \<in> - A\<close> for a b
    4.48 -    proof -
    4.49 -      from a have fa: \<open>f a \<in> f ` A\<close> by (rule imageI)
    4.50 -      from b have \<open>g' b \<in> g' ` (- A)\<close> by (rule imageI)
    4.51 -      with * have \<open>g' b \<in> - (f ` A)\<close> by simp
    4.52 -      with eq fa show \<open>False\<close> by simp
    4.53 -    qed
    4.54 -    ultimately show \<open>inj ?h\<close>
    4.55 -      unfolding inj_on_def by (metis ComplI)
    4.56 -  qed
    4.57 -qed
    4.58 -
    4.59 -end
     5.1 --- a/src/HOL/ROOT	Sat Oct 01 17:16:35 2016 +0200
     5.2 +++ b/src/HOL/ROOT	Sat Oct 01 17:38:14 2016 +0200
     5.3 @@ -644,7 +644,6 @@
     5.4      Peirce
     5.5      Drinker
     5.6      Cantor
     5.7 -    Schroeder_Bernstein
     5.8      Structured_Statements
     5.9      Basic_Logic
    5.10      Expr_Compiler