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>