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