src/HOL/Analysis/Continuum_Not_Denumerable.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      HOL/Analysis/Continuum_Not_Denumerable.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 Continuum_Not_Denumerable
     9 imports
    10   Complex_Main 
    11   "HOL-Library.Countable_Set"
    12 begin
    13 
    14 subsection%unimportant \<open>Abstract\<close>
    15 
    16 text \<open>
    17   The following document presents a proof that the Continuum is uncountable.
    18   It is formalised in the Isabelle/Isar theorem proving system.
    19 
    20   \<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does
    21   not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that \<open>f\<close> is surjective.
    22 
    23   \<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's
    24   Diagonalisation argument. The proof presented here is not this one.
    25 
    26   First we formalise some properties of closed intervals, then we prove the
    27   Nested Interval Property. This property relies on the completeness of the
    28   Real numbers and is the foundation for our argument. Informally it states
    29   that an intersection of countable closed intervals (where each successive
    30   interval is a subset of the last) is non-empty. We then assume a surjective
    31   function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the
    32   range of \<open>f\<close> by generating a sequence of closed intervals then using the
    33   Nested Interval Property.
    34 \<close>
    35 text%important \<open>%whitespace\<close>
    36 theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
    37 proof
    38   assume "\<exists>f::nat \<Rightarrow> real. surj f"
    39   then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
    40 
    41   txt \<open>First we construct a sequence of nested intervals, ignoring \<^term>\<open>range f\<close>.\<close>
    42 
    43   have "a < b \<Longrightarrow> \<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}" for a b c :: real
    44     by (auto simp add: not_le cong: conj_cong)
    45       (metis dense le_less_linear less_linear less_trans order_refl)
    46   then obtain i j where ij:
    47     "a < b \<Longrightarrow> i a b c < j a b c"
    48       "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
    49       "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
    50     for a b c :: real
    51     by metis
    52 
    53   define ivl where "ivl =
    54     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)))"
    55   define I where "I n = {fst (ivl n) .. snd (ivl n)}" for n
    56 
    57   have ivl [simp]:
    58     "ivl 0 = (f 0 + 1, f 0 + 2)"
    59     "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
    60     unfolding ivl_def by simp_all
    61 
    62   txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
    63 
    64   have less: "fst (ivl n) < snd (ivl n)" for n
    65     by (induct n) (auto intro!: ij)
    66 
    67   have "decseq I"
    68     unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv
    69     by (intro ij allI less)
    70 
    71   txt \<open>Now we apply the finite intersection property of compact sets.\<close>
    72 
    73   have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
    74   proof (rule compact_imp_fip_image)
    75     fix S :: "nat set"
    76     assume fin: "finite S"
    77     have "{} \<subset> I (Max (insert 0 S))"
    78       unfolding I_def using less[of "Max (insert 0 S)"] by auto
    79     also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
    80       using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"]
    81       by (auto simp: Max_ge_iff)
    82     also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
    83       by auto
    84     finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
    85       by auto
    86   qed (auto simp: I_def)
    87   then obtain x where "x \<in> I n" for n
    88     by blast
    89   moreover from \<open>surj f\<close> obtain j where "x = f j"
    90     by blast
    91   ultimately have "f j \<in> I (Suc j)"
    92     by blast
    93   with ij(3)[OF less] show False
    94     unfolding I_def ivl fst_conv snd_conv by auto
    95 qed
    96 
    97 lemma uncountable_UNIV_real: "uncountable (UNIV :: real set)"
    98   using real_non_denum unfolding uncountable_def by auto
    99 
   100 lemma bij_betw_open_intervals:
   101   fixes a b c d :: real
   102   assumes "a < b" "c < d"
   103   shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
   104 proof -
   105   define f where "f a b c d x = (d - c)/(b - a) * (x - a) + c" for a b c d x :: real
   106   {
   107     fix a b c d x :: real
   108     assume *: "a < b" "c < d" "a < x" "x < b"
   109     moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
   110       by (intro mult_strict_left_mono) simp_all
   111     moreover from * have "0 < (d - c) * (x - a) / (b - a)"
   112       by simp
   113     ultimately have "f a b c d x < d" "c < f a b c d x"
   114       by (simp_all add: f_def field_simps)
   115   }
   116   with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
   117     by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
   118   then show ?thesis by auto
   119 qed
   120 
   121 lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
   122   using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
   123 
   124 lemma uncountable_open_interval: "uncountable {a<..<b} \<longleftrightarrow> a < b" for a b :: real
   125 proof
   126   show "a < b" if "uncountable {a<..<b}"
   127     using uncountable_def that by force
   128   show "uncountable {a<..<b}" if "a < b"
   129   proof -
   130     obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
   131       using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
   132     then show ?thesis
   133       by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
   134   qed
   135 qed
   136 
   137 lemma uncountable_half_open_interval_1: "uncountable {a..<b} \<longleftrightarrow> a < b" for a b :: real
   138   apply auto
   139   using atLeastLessThan_empty_iff
   140   apply fastforce
   141   using uncountable_open_interval [of a b]
   142   apply (metis countable_Un_iff ivl_disj_un_singleton(3))
   143   done
   144 
   145 lemma uncountable_half_open_interval_2: "uncountable {a<..b} \<longleftrightarrow> a < b" for a b :: real
   146   apply auto
   147   using atLeastLessThan_empty_iff
   148   apply fastforce
   149   using uncountable_open_interval [of a b]
   150   apply (metis countable_Un_iff ivl_disj_un_singleton(4))
   151   done
   152 
   153 lemma real_interval_avoid_countable_set:
   154   fixes a b :: real and A :: "real set"
   155   assumes "a < b" and "countable A"
   156   shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
   157 proof -
   158   from \<open>countable A\<close> have *: "countable (A \<inter> {a<..<b})"
   159     by auto
   160   with \<open>a < b\<close> have "\<not> countable {a<..<b}"
   161     by (simp add: uncountable_open_interval)
   162   with * have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
   163     by auto
   164   then have "A \<inter> {a<..<b} \<subset> {a<..<b}"
   165     by (intro psubsetI) auto
   166   then have "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
   167     by (rule psubset_imp_ex_mem)
   168   then show ?thesis
   169     by auto
   170 qed
   171 
   172 lemma uncountable_closed_interval: "uncountable {a..b} \<longleftrightarrow> a < b" for a b :: real
   173   apply (rule iffI)
   174    apply (metis atLeastAtMost_singleton atLeastatMost_empty countable_finite finite.emptyI finite_insert linorder_neqE_linordered_idom)
   175   using real_interval_avoid_countable_set by fastforce
   176 
   177 lemma open_minus_countable:
   178   fixes S A :: "real set"
   179   assumes "countable A" "S \<noteq> {}" "open S"
   180   shows "\<exists>x\<in>S. x \<notin> A"
   181 proof -
   182   obtain x where "x \<in> S"
   183     using \<open>S \<noteq> {}\<close> by auto
   184   then obtain e where "0 < e" "{y. dist y x < e} \<subseteq> S"
   185     using \<open>open S\<close> by (auto simp: open_dist subset_eq)
   186   moreover have "{y. dist y x < e} = {x - e <..< x + e}"
   187     by (auto simp: dist_real_def)
   188   ultimately have "uncountable (S - A)"
   189     using uncountable_open_interval[of "x - e" "x + e"] \<open>countable A\<close>
   190     by (intro uncountable_minus_countable) (auto dest: countable_subset)
   191   then show ?thesis
   192     unfolding uncountable_def by auto
   193 qed
   194 
   195 end