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
```