src/HOL/Library/ContNotDenum.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62083 7582b39f51ed
child 63040 eb4ddd18d635
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     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 \<open>\<real>\<close> is not denumerable. In other
    19 words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> 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 \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real x such that x is not in the range of f
    30 by generating a sequence of closed intervals then using the NIP.\<close>
    31 
    32 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
    33 proof
    34   assume "\<exists>f::nat \<Rightarrow> real. surj f"
    35   then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
    36 
    37   txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
    38 
    39   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})"
    40     using assms
    41     by (auto simp add: not_le cong: conj_cong)
    42        (metis dense le_less_linear less_linear less_trans order_refl)
    43   then obtain i j where ij:
    44     "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
    45     "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
    46     "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
    47     by metis
    48 
    49   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)))"
    50   def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
    51 
    52   have ivl[simp]:
    53     "ivl 0 = (f 0 + 1, f 0 + 2)"
    54     "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
    55     unfolding ivl_def by simp_all
    56 
    57   txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
    58 
    59   { fix n have "fst (ivl n) < snd (ivl n)"
    60       by (induct n) (auto intro!: ij) }
    61   note less = this
    62 
    63   have "decseq I"
    64     unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
    65 
    66   txt \<open>Now we apply the finite intersection property of compact sets.\<close>
    67 
    68   have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
    69   proof (rule compact_imp_fip_image)
    70     fix S :: "nat set" assume fin: "finite S"
    71     have "{} \<subset> I (Max (insert 0 S))"
    72       unfolding I_def using less[of "Max (insert 0 S)"] by auto
    73     also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
    74       using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
    75     also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
    76       by auto
    77     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
    78       by auto
    79   qed (auto simp: I_def)
    80   then obtain x where "\<And>n. x \<in> I n"
    81     by blast
    82   moreover from \<open>surj f\<close> obtain j where "x = f j"
    83     by blast
    84   ultimately have "f j \<in> I (Suc j)"
    85     by blast
    86   with ij(3)[OF less] show False
    87     unfolding I_def ivl fst_conv snd_conv by auto
    88 qed
    89 
    90 lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
    91   using real_non_denum unfolding uncountable_def by auto
    92 
    93 lemma bij_betw_open_intervals:
    94   fixes a b c d :: real
    95   assumes "a < b" "c < d"
    96   shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
    97 proof -
    98   def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
    99   { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
   100     moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
   101       by (intro mult_strict_left_mono) simp_all
   102     moreover from * have "0 < (d - c) * (x - a) / (b - a)"
   103       by simp
   104     ultimately have "f a b c d x < d" "c < f a b c d x"
   105       by (simp_all add: f_def field_simps) }
   106   with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
   107     by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
   108   thus ?thesis by auto
   109 qed
   110 
   111 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
   112   using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
   113 
   114 lemma uncountable_open_interval:
   115   fixes a b :: real 
   116   shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
   117 proof
   118   assume "uncountable {a<..<b}"
   119   then show "a < b"
   120     using uncountable_def by force
   121 next 
   122   assume "a < b"
   123   show "uncountable {a<..<b}"
   124   proof -
   125     obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
   126       using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
   127     then show ?thesis
   128       by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
   129   qed
   130 qed
   131 
   132 lemma uncountable_half_open_interval_1:
   133   fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
   134   apply auto
   135   using atLeastLessThan_empty_iff apply fastforce
   136   using uncountable_open_interval [of a b]
   137   by (metis countable_Un_iff ivl_disj_un_singleton(3))
   138 
   139 lemma uncountable_half_open_interval_2:
   140   fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
   141   apply auto
   142   using atLeastLessThan_empty_iff apply fastforce
   143   using uncountable_open_interval [of a b]
   144   by (metis countable_Un_iff ivl_disj_un_singleton(4))
   145 
   146 lemma real_interval_avoid_countable_set:
   147   fixes a b :: real and A :: "real set"
   148   assumes "a < b" and "countable A"
   149   shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
   150 proof -
   151   from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" by auto
   152   moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}" 
   153     by (simp add: uncountable_open_interval)
   154   ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
   155   hence "A \<inter> {a<..<b} \<subset> {a<..<b}" 
   156     by (intro psubsetI, auto)
   157   hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
   158     by (rule psubset_imp_ex_mem)
   159   thus ?thesis by auto
   160 qed
   161 
   162 lemma open_minus_countable:
   163   fixes S A :: "real set" assumes "countable A" "S \<noteq> {}" "open S"
   164   shows "\<exists>x\<in>S. x \<notin> A"
   165 proof -
   166   obtain x where "x \<in> S"
   167     using \<open>S \<noteq> {}\<close> by auto
   168   then obtain e where "0 < e" "{y. dist y x < e} \<subseteq> S"
   169     using \<open>open S\<close> by (auto simp: open_dist subset_eq)
   170   moreover have "{y. dist y x < e} = {x - e <..< x + e}"
   171     by (auto simp: dist_real_def)
   172   ultimately have "uncountable (S - A)"
   173     using uncountable_open_interval[of "x - e" "x + e"] \<open>countable A\<close>
   174     by (intro uncountable_minus_countable) (auto dest: countable_subset)
   175   then show ?thesis
   176     unfolding uncountable_def by auto
   177 qed
   178 
   179 end