# HG changeset patch
# User wenzelm
# Date 1475336294 7200
# Node ID f8e556c8ad6ffb97712bbd5e8ea28352e3690b8b
# Parent 95c3ae4baba8d37bfbd48c88c14ffef77b15aa50
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
diff r 95c3ae4baba8 r f8e556c8ad6f src/HOL/BNF_Cardinal_Order_Relation.thy
 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 \o B" using ordIso_iff_ordLeq by auto
}
diff r 95c3ae4baba8 r f8e556c8ad6f src/HOL/Hilbert_Choice.thy
 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 \The CantorBernstein Theorem\

lemma Cantor_Bernstein_aux:
 "\A' h. A' \ A \
 (\a \ A'. a \ g ` (B  f ` A')) \
 (\a \ A'. h a = f a) \
 (\a \ A  A'. h a \ B  (f ` A') \ 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' \ A"
 and 2: "\a \ A'. a \ g ` (B  f ` A')"
 and 3: "\a \ A  A'. \b \ B  (f ` A'). a = g b"
 by blast+
 define h where "h a = (if a \ A' then f a else (SOME b. b \ B  (f ` A') \ a = g b))" for a
 then have 4: "\a \ A'. h a = f a" by simp
 have "\a \ A  A'. h a \ B  (f ` A') \ a = g (h a)"
 proof
 fix a
 let ?phi = "\b. b \ B  (f ` A') \ a = g b"
 assume *: "a \ A  A'"
 from * have "h a = (SOME b. ?phi b)" by (auto simp: h_def)
 moreover from 3 * have "\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 \ B"
 and inj2: "inj_on g B" and sub2: "g ` B \ A"
 shows "\h. bij_betw h A B"
proof
 obtain A' and h where "A' \ A"
 and 1: "\a \ A'. a \ g ` (B  f ` A')"
 and 2: "\a \ A'. h a = f a"
 and 3: "\a \ A  A'. h a \ B  (f ` A') \ 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 \ A" and 5: "a2 \ A" and 6: "h a1 = h a2"
 show "a1 = a2"
 proof (cases "a1 \ A'")
 case True
 show ?thesis
 proof (cases "a2 \ A'")
 case True': True
 with True 2 6 have "f a1 = f a2" by auto
 with inj1 \A' \ A\ 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 \ 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 \ A"
 with sub1 2 3 show "h a \ B" by (cases "a \ A'") auto
 next
 fix b
 assume *: "b \ B"
 show "b \ h ` A"
 proof (cases "b \ f ` A'")
 case True
 then obtain a where "a \ A'" "b = f a" by blast
 with \A' \ A\ 2 show ?thesis by force
 next
 case False
 with 1 * have "g b \ A'" by auto
 with sub2 * have 4: "g b \ A  A'" by auto
 with 3 have "h (g b) \ 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 \Other Consequences of Hilbert's Epsilon\
text \Hilbert's Epsilon and the @{term split} Operator\
diff r 95c3ae4baba8 r f8e556c8ad6f src/HOL/Inductive.thy
 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 \The SchroederBernstein Theorem\
+
+text \
+ See also:
+ \<^item> \<^file>\$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\
+ \<^item> \<^url>\http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\
+ \<^item> Springer LNCS 828 (cover page)
+\
+
+theorem Schroeder_Bernstein:
+ fixes f :: "'a \ 'b" and g :: "'b \ 'a"
+ and A :: "'a set" and B :: "'b set"
+ assumes inj1: "inj_on f A" and sub1: "f ` A \ B"
+ and inj2: "inj_on g B" and sub2: "g ` B \ A"
+ shows "\h. bij_betw h A B"
+proof (rule exI, rule bij_betw_imageI)
+ define X where "X = lfp (\X. A  (g ` (B  (f ` X))))"
+ define g' where "g' = the_inv_into (B  (f ` X)) g"
+ let ?h = "\z. if z \ 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 \ A" by auto
+ from X sub1 have fX_sub: "f ` X \ B" by auto
+
+ show "?h ` A = B"
+ proof 
+ from X_sub have "?h ` A = ?h ` (X \ (A  X))" by auto
+ also have "\ = ?h ` X \ ?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 \ (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 \ X" and b: "b \ A  X" for a b
+ proof 
+ from a have fa: "f a \ f ` X" by (rule imageI)
+ from b have "g' b \ g' ` (A  X)" by (rule imageI)
+ with * have "g' b \  (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 \ A" and "b \ A"
+ then consider "a \ X" "b \ X"  "a \ A  X" "b \ A  X"
+  "a \ X" "b \ A  X"  "a \ A  X" "b \ 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 \Inductive datatypes and primitive recursion\
text \Package setup.\
diff r 95c3ae4baba8 r f8e556c8ad6f src/HOL/Isar_Examples/Schroeder_Bernstein.thy
 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 \SchrÃ¶derBernstein Theorem\

theory Schroeder_Bernstein
 imports Main
begin

text \
 See also:
 \<^item> \<^file>\$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\
 \<^item> \<^url>\http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\
 \<^item> Springer LNCS 828 (cover page)
\

theorem Schroeder_Bernstein: \\h :: 'a \ 'b. inj h \ surj h\ if \inj f\ and \inj g\
 for f :: \'a \ 'b\ and g :: \'b \ 'a\
proof
 define A where \A = lfp (\X.  (g ` ( (f ` X))))\
 define g' where \g' = inv g\
 let \?h\ = \\z. if z \ A then f z else g' z\

 have \A =  (g ` ( (f ` A)))\
 unfolding A_def by (rule lfp_unfold) (blast intro: monoI)
 then have A_compl: \ A = g ` ( (f ` A))\ by blast
 then have *: \g' ` ( A) =  (f ` A)\
 using g'_def \inj g\ by auto

 show \inj ?h \ surj ?h\
 proof
 from * show \surj ?h\ by auto
 have \inj_on f A\
 using \inj f\ by (rule subset_inj_on) blast
 moreover
 have \inj_on g' ( A)\
 unfolding g'_def
 proof (rule inj_on_inv_into)
 have \g ` ( (f ` A)) \ range g\ by blast
 then show \ A \ range g\ by (simp only: A_compl)
 qed
 moreover
 have \False\ if eq: \f a = g' b\ and a: \a \ A\ and b: \b \  A\ for a b
 proof 
 from a have fa: \f a \ f ` A\ by (rule imageI)
 from b have \g' b \ g' ` ( A)\ by (rule imageI)
 with * have \g' b \  (f ` A)\ by simp
 with eq fa show \False\ by simp
 qed
 ultimately show \inj ?h\
 unfolding inj_on_def by (metis ComplI)
 qed
qed

end
diff r 95c3ae4baba8 r f8e556c8ad6f src/HOL/ROOT
 a/src/HOL/ROOT Sat Oct 01 17:16:35 2016 +0200
+++ b/src/HOL/ROOT Sat Oct 01 17:38:14 2016 +0200
@@ 644,7 +644,6 @@
Peirce
Drinker
Cantor
 Schroeder_Bernstein
Structured_Statements
Basic_Logic
Expr_Compiler