summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 01 Oct 2016 17:38:14 +0200 | |

changeset 63980 | f8e556c8ad6f |

parent 63979 | 95c3ae4baba8 |

child 63981 | 6f7db4f8df4c |

Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);

src/HOL/BNF_Cardinal_Order_Relation.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Hilbert_Choice.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Inductive.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_Examples/Schroeder_Bernstein.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ROOT | file | annotate | diff | comparison | revisions |

--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sat Oct 01 17:16:35 2016 +0200 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Sat Oct 01 17:38:14 2016 +0200 @@ -183,7 +183,7 @@ card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"] embed_Field[of "|B|" "|A|" g] by auto obtain h where "bij_betw h A B" - using * ** 1 Cantor_Bernstein[of f] by fastforce + using * ** 1 Schroeder_Bernstein[of f] by fastforce hence "|A| =o |B|" using card_of_ordIso by blast hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto }

--- a/src/HOL/Hilbert_Choice.thy Sat Oct 01 17:16:35 2016 +0200 +++ b/src/HOL/Hilbert_Choice.thy Sat Oct 01 17:38:14 2016 +0200 @@ -450,106 +450,6 @@ using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff) -subsection \<open>The Cantor-Bernstein Theorem\<close> - -lemma Cantor_Bernstein_aux: - "\<exists>A' h. A' \<subseteq> A \<and> - (\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')) \<and> - (\<forall>a \<in> A'. h a = f a) \<and> - (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a))" -proof - - define H where "H A' = A - (g ` (B - (f ` A')))" for A' - have "mono H" unfolding mono_def H_def by blast - from lfp_unfold [OF this] obtain A' where "H A' = A'" by blast - then have "A' = A - (g ` (B - (f ` A')))" by (simp add: H_def) - then have 1: "A' \<subseteq> A" - and 2: "\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')" - and 3: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b" - by blast+ - 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 - then have 4: "\<forall>a \<in> A'. h a = f a" by simp - have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)" - proof - fix a - let ?phi = "\<lambda>b. b \<in> B - (f ` A') \<and> a = g b" - assume *: "a \<in> A - A'" - from * have "h a = (SOME b. ?phi b)" by (auto simp: h_def) - moreover from 3 * have "\<exists>b. ?phi b" by auto - ultimately show "?phi (h a)" - using someI_ex[of ?phi] by auto - qed - with 1 2 4 show ?thesis by blast -qed - -theorem Cantor_Bernstein: - assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B" - and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A" - shows "\<exists>h. bij_betw h A B" -proof- - obtain A' and h where "A' \<subseteq> A" - and 1: "\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')" - and 2: "\<forall>a \<in> A'. h a = f a" - and 3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)" - using Cantor_Bernstein_aux [of A g B f] by blast - have "inj_on h A" - proof (intro inj_onI) - fix a1 a2 - assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2" - show "a1 = a2" - proof (cases "a1 \<in> A'") - case True - show ?thesis - proof (cases "a2 \<in> A'") - case True': True - with True 2 6 have "f a1 = f a2" by auto - with inj1 \<open>A' \<subseteq> A\<close> True True' show ?thesis - unfolding inj_on_def by blast - next - case False - with 2 3 5 6 True have False by force - then show ?thesis .. - qed - next - case False - show ?thesis - proof (cases "a2 \<in> A'") - case True - with 2 3 4 6 False have False by auto - then show ?thesis .. - next - case False': False - with False 3 4 5 have "a1 = g (h a1)" "a2 = g (h a2)" by auto - with 6 show ?thesis by simp - qed - qed - qed - moreover have "h ` A = B" - proof safe - fix a - assume "a \<in> A" - with sub1 2 3 show "h a \<in> B" by (cases "a \<in> A'") auto - next - fix b - assume *: "b \<in> B" - show "b \<in> h ` A" - proof (cases "b \<in> f ` A'") - case True - then obtain a where "a \<in> A'" "b = f a" by blast - with \<open>A' \<subseteq> A\<close> 2 show ?thesis by force - next - case False - with 1 * have "g b \<notin> A'" by auto - with sub2 * have 4: "g b \<in> A - A'" by auto - with 3 have "h (g b) \<in> B" "g (h (g b)) = g b" by auto - with inj2 * have "h (g b) = b" by (auto simp: inj_on_def) - with 4 show ?thesis by force - qed - qed - ultimately show ?thesis - by (auto simp: bij_betw_def) -qed - - subsection \<open>Other Consequences of Hilbert's Epsilon\<close> text \<open>Hilbert's Epsilon and the @{term split} Operator\<close>

--- a/src/HOL/Inductive.thy Sat Oct 01 17:16:35 2016 +0200 +++ b/src/HOL/Inductive.thy Sat Oct 01 17:38:14 2016 +0200 @@ -422,6 +422,94 @@ induct_rulify_fallback +subsection \<open>The Schroeder-Bernstein Theorem\<close> + +text \<open> + See also: + \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close> + \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close> + \<^item> Springer LNCS 828 (cover page) +\<close> + +theorem Schroeder_Bernstein: + fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a" + and A :: "'a set" and B :: "'b set" + assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B" + and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A" + shows "\<exists>h. bij_betw h A B" +proof (rule exI, rule bij_betw_imageI) + define X where "X = lfp (\<lambda>X. A - (g ` (B - (f ` X))))" + define g' where "g' = the_inv_into (B - (f ` X)) g" + let ?h = "\<lambda>z. if z \<in> X then f z else g' z" + + have X: "X = A - (g ` (B - (f ` X)))" + unfolding X_def by (rule lfp_unfold) (blast intro: monoI) + then have X_compl: "A - X = g ` (B - (f ` X))" + using sub2 by blast + + from inj2 have inj2': "inj_on g (B - (f ` X))" + by (rule inj_on_subset) auto + with X_compl have *: "g' ` (A - X) = B - (f ` X)" + by (simp add: g'_def) + + from X have X_sub: "X \<subseteq> A" by auto + from X sub1 have fX_sub: "f ` X \<subseteq> B" by auto + + show "?h ` A = B" + proof - + from X_sub have "?h ` A = ?h ` (X \<union> (A - X))" by auto + also have "\<dots> = ?h ` X \<union> ?h ` (A - X)" by (simp only: image_Un) + also have "?h ` X = f ` X" by auto + also from * have "?h ` (A - X) = B - (f ` X)" by auto + also from fX_sub have "f ` X \<union> (B - f ` X) = B" by blast + finally show ?thesis . + qed + show "inj_on ?h A" + proof - + from inj1 X_sub have on_X: "inj_on f X" + by (rule subset_inj_on) + + have on_X_compl: "inj_on g' (A - X)" + unfolding g'_def X_compl + by (rule inj_on_the_inv_into) (rule inj2') + + have impossible: False if eq: "f a = g' b" and a: "a \<in> X" and b: "b \<in> A - X" for a b + proof - + from a have fa: "f a \<in> f ` X" by (rule imageI) + from b have "g' b \<in> g' ` (A - X)" by (rule imageI) + with * have "g' b \<in> - (f ` X)" by simp + with eq fa show False by simp + qed + + show ?thesis + proof (rule inj_onI) + fix a b + assume h: "?h a = ?h b" + assume "a \<in> A" and "b \<in> A" + then consider "a \<in> X" "b \<in> X" | "a \<in> A - X" "b \<in> A - X" + | "a \<in> X" "b \<in> A - X" | "a \<in> A - X" "b \<in> X" + by blast + then show "a = b" + proof cases + case 1 + with h on_X show ?thesis by (simp add: inj_on_eq_iff) + next + case 2 + with h on_X_compl show ?thesis by (simp add: inj_on_eq_iff) + next + case 3 + with h impossible [of a b] have False by simp + then show ?thesis .. + next + case 4 + with h impossible [of b a] have False by simp + then show ?thesis .. + qed + qed + qed +qed + + subsection \<open>Inductive datatypes and primitive recursion\<close> text \<open>Package setup.\<close>

--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Sat Oct 01 17:16:35 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,56 +0,0 @@ -(* Title: HOL/Isar_Examples/Schroeder_Bernstein.thy - Author: Makarius -*) - -section \<open>SchrÃ¶der-Bernstein Theorem\<close> - -theory Schroeder_Bernstein - imports Main -begin - -text \<open> - See also: - \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close> - \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close> - \<^item> Springer LNCS 828 (cover page) -\<close> - -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> - for f :: \<open>'a \<Rightarrow> 'b\<close> and g :: \<open>'b \<Rightarrow> 'a\<close> -proof - define A where \<open>A = lfp (\<lambda>X. - (g ` (- (f ` X))))\<close> - define g' where \<open>g' = inv g\<close> - let \<open>?h\<close> = \<open>\<lambda>z. if z \<in> A then f z else g' z\<close> - - have \<open>A = - (g ` (- (f ` A)))\<close> - unfolding A_def by (rule lfp_unfold) (blast intro: monoI) - then have A_compl: \<open>- A = g ` (- (f ` A))\<close> by blast - then have *: \<open>g' ` (- A) = - (f ` A)\<close> - using g'_def \<open>inj g\<close> by auto - - show \<open>inj ?h \<and> surj ?h\<close> - proof - from * show \<open>surj ?h\<close> by auto - have \<open>inj_on f A\<close> - using \<open>inj f\<close> by (rule subset_inj_on) blast - moreover - have \<open>inj_on g' (- A)\<close> - unfolding g'_def - proof (rule inj_on_inv_into) - have \<open>g ` (- (f ` A)) \<subseteq> range g\<close> by blast - then show \<open>- A \<subseteq> range g\<close> by (simp only: A_compl) - qed - moreover - 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 - proof - - from a have fa: \<open>f a \<in> f ` A\<close> by (rule imageI) - from b have \<open>g' b \<in> g' ` (- A)\<close> by (rule imageI) - with * have \<open>g' b \<in> - (f ` A)\<close> by simp - with eq fa show \<open>False\<close> by simp - qed - ultimately show \<open>inj ?h\<close> - unfolding inj_on_def by (metis ComplI) - qed -qed - -end