src/HOL/Library/ContNotDenum.thy
 author hoelzl Thu Dec 17 16:43:36 2015 +0100 (2015-12-17) changeset 61880 ff4d33058566 parent 61585 a9599d3d7610 child 61975 b4b11391c676 permissions -rw-r--r--
moved some theorems from the CLT proof; reordered some theorems / notation
 wenzelm@59720  1 (* Title: HOL/Library/ContNotDenum.thy  wenzelm@56796  2  Author: Benjamin Porter, Monash University, NICTA, 2005  hoelzl@57234  3  Author: Johannes Hölzl, TU München  wenzelm@23461  4 *)  wenzelm@23461  5 wenzelm@60500  6 section \Non-denumerability of the Continuum.\  wenzelm@23461  7 wenzelm@23461  8 theory ContNotDenum  hoelzl@57234  9 imports Complex_Main Countable_Set  wenzelm@23461  10 begin  wenzelm@23461  11 wenzelm@60500  12 subsection \Abstract\  wenzelm@23461  13 wenzelm@60500  14 text \The following document presents a proof that the Continuum is  wenzelm@23461  15 uncountable. It is formalised in the Isabelle/Isar theorem proving  wenzelm@23461  16 system.  wenzelm@23461  17 wenzelm@61585  18 {\em Theorem:} The Continuum \\\ is not denumerable. In other  wenzelm@61585  19 words, there does not exist a function \f: \ \ \\ such that f is  wenzelm@23461  20 surjective.  wenzelm@23461  21 wenzelm@23461  22 {\em Outline:} An elegant informal proof of this result uses Cantor's  wenzelm@23461  23 Diagonalisation argument. The proof presented here is not this  wenzelm@23461  24 one. First we formalise some properties of closed intervals, then we  wenzelm@23461  25 prove the Nested Interval Property. This property relies on the  wenzelm@23461  26 completeness of the Real numbers and is the foundation for our  wenzelm@23461  27 argument. Informally it states that an intersection of countable  wenzelm@23461  28 closed intervals (where each successive interval is a subset of the  wenzelm@61585  29 last) is non-empty. We then assume a surjective function \f: \ \ \\ exists and find a real x such that x is not in the range of f  wenzelm@60500  30 by generating a sequence of closed intervals then using the NIP.\  wenzelm@23461  31 hoelzl@57234  32 theorem real_non_denum: "\ (\f :: nat \ real. surj f)"  hoelzl@57234  33 proof  hoelzl@57234  34  assume "\f::nat \ real. surj f"  hoelzl@57234  35  then obtain f :: "nat \ real" where "surj f" ..  wenzelm@56796  36 wenzelm@60500  37  txt \First we construct a sequence of nested intervals, ignoring @{term "range f"}.\  wenzelm@23461  38 hoelzl@57234  39  have "\a b c::real. a < b \ (\ka kb. ka < kb \ {ka..kb} \ {a..b} \ c \ {ka..kb})"  hoelzl@57234  40  using assms  hoelzl@57234  41  by (auto simp add: not_le cong: conj_cong)  hoelzl@57234  42  (metis dense le_less_linear less_linear less_trans order_refl)  hoelzl@57234  43  then obtain i j where ij:  hoelzl@57234  44  "\a b c::real. a < b \ i a b c < j a b c"  hoelzl@57234  45  "\a b c. a < b \ {i a b c .. j a b c} \ {a .. b}"  hoelzl@57234  46  "\a b c. a < b \ c \ {i a b c .. j a b c}"  hoelzl@57234  47  by metis  wenzelm@23461  48 hoelzl@57234  49  def ivl \ "rec_nat (f 0 + 1, f 0 + 2) (\n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"  hoelzl@57234  50  def I \ "\n. {fst (ivl n) .. snd (ivl n)}"  wenzelm@23461  51 hoelzl@57234  52  have ivl[simp]:  hoelzl@57234  53  "ivl 0 = (f 0 + 1, f 0 + 2)"  hoelzl@57234  54  "\n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"  hoelzl@57234  55  unfolding ivl_def by simp_all  wenzelm@56796  56 wenzelm@60500  57  txt \This is a decreasing sequence of non-empty intervals.\  wenzelm@23461  58 hoelzl@57234  59  { fix n have "fst (ivl n) < snd (ivl n)"  hoelzl@57234  60  by (induct n) (auto intro!: ij) }  hoelzl@57234  61  note less = this  wenzelm@23461  62 hoelzl@57234  63  have "decseq I"  hoelzl@57234  64  unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)  hoelzl@57234  65 wenzelm@60500  66  txt \Now we apply the finite intersection property of compact sets.\  wenzelm@23461  67 hoelzl@57234  68  have "I 0 \ (\i. I i) \ {}"  hoelzl@57234  69  proof (rule compact_imp_fip_image)  hoelzl@57234  70  fix S :: "nat set" assume fin: "finite S"  hoelzl@57234  71  have "{} \ I (Max (insert 0 S))"  hoelzl@57234  72  unfolding I_def using less[of "Max (insert 0 S)"] by auto  hoelzl@57234  73  also have "I (Max (insert 0 S)) \ (\i\insert 0 S. I i)"  wenzelm@60500  74  using fin decseqD[OF \decseq I\, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)  hoelzl@57234  75  also have "(\i\insert 0 S. I i) = I 0 \ (\i\S. I i)"  wenzelm@56796  76  by auto  hoelzl@57234  77  finally show "I 0 \ (\i\S. I i) \ {}"  wenzelm@53372  78  by auto  hoelzl@57234  79  qed (auto simp: I_def)  hoelzl@57234  80  then obtain x where "\n. x \ I n"  hoelzl@57234  81  by blast  wenzelm@60500  82  moreover from \surj f\ obtain j where "x = f j"  hoelzl@57234  83  by blast  hoelzl@57234  84  ultimately have "f j \ I (Suc j)"  hoelzl@57234  85  by blast  hoelzl@57234  86  with ij(3)[OF less] show False  hoelzl@57234  87  unfolding I_def ivl fst_conv snd_conv by auto  wenzelm@23461  88 qed  wenzelm@23461  89 hoelzl@57234  90 lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"  hoelzl@57234  91  using real_non_denum unfolding uncountable_def by auto  wenzelm@23461  92 hoelzl@57234  93 lemma bij_betw_open_intervals:  hoelzl@57234  94  fixes a b c d :: real  hoelzl@57234  95  assumes "a < b" "c < d"  hoelzl@57234  96  shows "\f. bij_betw f {a<.. "\a b c d x::real. (d - c)/(b - a) * (x - a) + c"  hoelzl@57234  99  { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"  hoelzl@57234  100  moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"  hoelzl@57234  101  by (intro mult_strict_left_mono) simp_all  hoelzl@57234  102  moreover from * have "0 < (d - c) * (x - a) / (b - a)"  hoelzl@57234  103  by simp  hoelzl@57234  104  ultimately have "f a b c d x < d" "c < f a b c d x"  hoelzl@57234  105  by (simp_all add: f_def field_simps) }  hoelzl@57234  106  with assms have "bij_betw (f a b c d) {a<.. a < b"  lp15@60308  117 proof  lp15@60308  118  assume "uncountable {a<..a < b\, of "-pi/2" "pi/2"] by auto  lp15@60308  127  then show ?thesis  lp15@60308  128  by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)  lp15@60308  129  qed  wenzelm@23461  130 qed  wenzelm@23461  131 lp15@60308  132 lemma uncountable_half_open_interval_1:  lp15@60308  133  fixes a :: real shows "uncountable {a.. a ax\{a<.. A"  hoelzl@61880  150 proof -  hoelzl@61880  151  from countable A` have "countable (A \ {a<.. countable {a<.. {a<.. {a<.. {a<.. {a<..x. x \ {a<.. {a<..