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