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>
```