summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Hilbert_Choice.thy

changeset 63980 | f8e556c8ad6f |

parent 63807 | 5f77017055a3 |

child 63981 | 6f7db4f8df4c |

1.1 --- a/src/HOL/Hilbert_Choice.thy Sat Oct 01 17:16:35 2016 +0200 1.2 +++ b/src/HOL/Hilbert_Choice.thy Sat Oct 01 17:38:14 2016 +0200 1.3 @@ -450,106 +450,6 @@ 1.4 using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff) 1.5 1.6 1.7 -subsection \<open>The Cantor-Bernstein Theorem\<close> 1.8 - 1.9 -lemma Cantor_Bernstein_aux: 1.10 - "\<exists>A' h. A' \<subseteq> A \<and> 1.11 - (\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')) \<and> 1.12 - (\<forall>a \<in> A'. h a = f a) \<and> 1.13 - (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a))" 1.14 -proof - 1.15 - define H where "H A' = A - (g ` (B - (f ` A')))" for A' 1.16 - have "mono H" unfolding mono_def H_def by blast 1.17 - from lfp_unfold [OF this] obtain A' where "H A' = A'" by blast 1.18 - then have "A' = A - (g ` (B - (f ` A')))" by (simp add: H_def) 1.19 - then have 1: "A' \<subseteq> A" 1.20 - and 2: "\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')" 1.21 - and 3: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b" 1.22 - by blast+ 1.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 1.24 - then have 4: "\<forall>a \<in> A'. h a = f a" by simp 1.25 - have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)" 1.26 - proof 1.27 - fix a 1.28 - let ?phi = "\<lambda>b. b \<in> B - (f ` A') \<and> a = g b" 1.29 - assume *: "a \<in> A - A'" 1.30 - from * have "h a = (SOME b. ?phi b)" by (auto simp: h_def) 1.31 - moreover from 3 * have "\<exists>b. ?phi b" by auto 1.32 - ultimately show "?phi (h a)" 1.33 - using someI_ex[of ?phi] by auto 1.34 - qed 1.35 - with 1 2 4 show ?thesis by blast 1.36 -qed 1.37 - 1.38 -theorem Cantor_Bernstein: 1.39 - assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B" 1.40 - and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A" 1.41 - shows "\<exists>h. bij_betw h A B" 1.42 -proof- 1.43 - obtain A' and h where "A' \<subseteq> A" 1.44 - and 1: "\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')" 1.45 - and 2: "\<forall>a \<in> A'. h a = f a" 1.46 - and 3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)" 1.47 - using Cantor_Bernstein_aux [of A g B f] by blast 1.48 - have "inj_on h A" 1.49 - proof (intro inj_onI) 1.50 - fix a1 a2 1.51 - assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2" 1.52 - show "a1 = a2" 1.53 - proof (cases "a1 \<in> A'") 1.54 - case True 1.55 - show ?thesis 1.56 - proof (cases "a2 \<in> A'") 1.57 - case True': True 1.58 - with True 2 6 have "f a1 = f a2" by auto 1.59 - with inj1 \<open>A' \<subseteq> A\<close> True True' show ?thesis 1.60 - unfolding inj_on_def by blast 1.61 - next 1.62 - case False 1.63 - with 2 3 5 6 True have False by force 1.64 - then show ?thesis .. 1.65 - qed 1.66 - next 1.67 - case False 1.68 - show ?thesis 1.69 - proof (cases "a2 \<in> A'") 1.70 - case True 1.71 - with 2 3 4 6 False have False by auto 1.72 - then show ?thesis .. 1.73 - next 1.74 - case False': False 1.75 - with False 3 4 5 have "a1 = g (h a1)" "a2 = g (h a2)" by auto 1.76 - with 6 show ?thesis by simp 1.77 - qed 1.78 - qed 1.79 - qed 1.80 - moreover have "h ` A = B" 1.81 - proof safe 1.82 - fix a 1.83 - assume "a \<in> A" 1.84 - with sub1 2 3 show "h a \<in> B" by (cases "a \<in> A'") auto 1.85 - next 1.86 - fix b 1.87 - assume *: "b \<in> B" 1.88 - show "b \<in> h ` A" 1.89 - proof (cases "b \<in> f ` A'") 1.90 - case True 1.91 - then obtain a where "a \<in> A'" "b = f a" by blast 1.92 - with \<open>A' \<subseteq> A\<close> 2 show ?thesis by force 1.93 - next 1.94 - case False 1.95 - with 1 * have "g b \<notin> A'" by auto 1.96 - with sub2 * have 4: "g b \<in> A - A'" by auto 1.97 - with 3 have "h (g b) \<in> B" "g (h (g b)) = g b" by auto 1.98 - with inj2 * have "h (g b) = b" by (auto simp: inj_on_def) 1.99 - with 4 show ?thesis by force 1.100 - qed 1.101 - qed 1.102 - ultimately show ?thesis 1.103 - by (auto simp: bij_betw_def) 1.104 -qed 1.105 - 1.106 - 1.107 subsection \<open>Other Consequences of Hilbert's Epsilon\<close> 1.108 1.109 text \<open>Hilbert's Epsilon and the @{term split} Operator\<close>