src/HOL/Library/ContNotDenum.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 60500 903bb1495239
child 61585 a9599d3d7610
permissions -rw-r--r--
tuned references
     1 (*  Title:      HOL/Library/ContNotDenum.thy
     2     Author:     Benjamin Porter, Monash University, NICTA, 2005
     3     Author:     Johannes Hölzl, TU München
     4 *)
     5 
     6 section \<open>Non-denumerability of the Continuum.\<close>
     7 
     8 theory ContNotDenum
     9 imports Complex_Main Countable_Set
    10 begin
    11 
    12 subsection \<open>Abstract\<close>
    13 
    14 text \<open>The following document presents a proof that the Continuum is
    15 uncountable. It is formalised in the Isabelle/Isar theorem proving
    16 system.
    17 
    18 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    19 words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
    20 surjective.
    21 
    22 {\em Outline:} An elegant informal proof of this result uses Cantor's
    23 Diagonalisation argument. The proof presented here is not this
    24 one. First we formalise some properties of closed intervals, then we
    25 prove the Nested Interval Property. This property relies on the
    26 completeness of the Real numbers and is the foundation for our
    27 argument. Informally it states that an intersection of countable
    28 closed intervals (where each successive interval is a subset of the
    29 last) is non-empty. We then assume a surjective function @{text
    30 "f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
    31 by generating a sequence of closed intervals then using the NIP.\<close>
    32 
    33 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
    34 proof
    35   assume "\<exists>f::nat \<Rightarrow> real. surj f"
    36   then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
    37 
    38   txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
    39 
    40   have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
    41     using assms
    42     by (auto simp add: not_le cong: conj_cong)
    43        (metis dense le_less_linear less_linear less_trans order_refl)
    44   then obtain i j where ij:
    45     "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
    46     "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
    47     "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
    48     by metis
    49 
    50   def ivl \<equiv> "rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
    51   def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
    52 
    53   have ivl[simp]:
    54     "ivl 0 = (f 0 + 1, f 0 + 2)"
    55     "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
    56     unfolding ivl_def by simp_all
    57 
    58   txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
    59 
    60   { fix n have "fst (ivl n) < snd (ivl n)"
    61       by (induct n) (auto intro!: ij) }
    62   note less = this
    63 
    64   have "decseq I"
    65     unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
    66 
    67   txt \<open>Now we apply the finite intersection property of compact sets.\<close>
    68 
    69   have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
    70   proof (rule compact_imp_fip_image)
    71     fix S :: "nat set" assume fin: "finite S"
    72     have "{} \<subset> I (Max (insert 0 S))"
    73       unfolding I_def using less[of "Max (insert 0 S)"] by auto
    74     also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
    75       using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
    76     also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
    77       by auto
    78     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
    79       by auto
    80   qed (auto simp: I_def)
    81   then obtain x where "\<And>n. x \<in> I n"
    82     by blast
    83   moreover from \<open>surj f\<close> obtain j where "x = f j"
    84     by blast
    85   ultimately have "f j \<in> I (Suc j)"
    86     by blast
    87   with ij(3)[OF less] show False
    88     unfolding I_def ivl fst_conv snd_conv by auto
    89 qed
    90 
    91 lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
    92   using real_non_denum unfolding uncountable_def by auto
    93 
    94 lemma bij_betw_open_intervals:
    95   fixes a b c d :: real
    96   assumes "a < b" "c < d"
    97   shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
    98 proof -
    99   def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
   100   { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
   101     moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
   102       by (intro mult_strict_left_mono) simp_all
   103     moreover from * have "0 < (d - c) * (x - a) / (b - a)"
   104       by simp
   105     ultimately have "f a b c d x < d" "c < f a b c d x"
   106       by (simp_all add: f_def field_simps) }
   107   with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
   108     by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
   109   thus ?thesis by auto
   110 qed
   111 
   112 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
   113   using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
   114 
   115 lemma uncountable_open_interval:
   116   fixes a b :: real 
   117   shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
   118 proof
   119   assume "uncountable {a<..<b}"
   120   then show "a < b"
   121     using uncountable_def by force
   122 next 
   123   assume "a < b"
   124   show "uncountable {a<..<b}"
   125   proof -
   126     obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
   127       using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
   128     then show ?thesis
   129       by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
   130   qed
   131 qed
   132 
   133 lemma uncountable_half_open_interval_1:
   134   fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
   135   apply auto
   136   using atLeastLessThan_empty_iff apply fastforce
   137   using uncountable_open_interval [of a b]
   138   by (metis countable_Un_iff ivl_disj_un_singleton(3))
   139 
   140 lemma uncountable_half_open_interval_2:
   141   fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
   142   apply auto
   143   using atLeastLessThan_empty_iff apply fastforce
   144   using uncountable_open_interval [of a b]
   145   by (metis countable_Un_iff ivl_disj_un_singleton(4))
   146 
   147 end