src/HOL/Library/ContNotDenum.thy
author paulson <lp15@cam.ac.uk>
Fri May 29 14:35:59 2015 +0100 (2015-05-29)
changeset 60308 f7e406aba90d
parent 59872 db4000b71fdb
child 60500 903bb1495239
permissions -rw-r--r--
uncountability: open interval equivalences
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@58881
     6
section {* Non-denumerability of the Continuum. *}
wenzelm@23461
     7
wenzelm@23461
     8
theory ContNotDenum
hoelzl@57234
     9
imports Complex_Main Countable_Set
wenzelm@23461
    10
begin
wenzelm@23461
    11
wenzelm@23461
    12
subsection {* Abstract *}
wenzelm@23461
    13
wenzelm@23461
    14
text {* 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@23461
    18
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
wenzelm@56796
    19
words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} 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@56796
    29
last) is non-empty. We then assume a surjective function @{text
wenzelm@56796
    30
"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
wenzelm@23461
    31
by generating a sequence of closed intervals then using the NIP. *}
wenzelm@23461
    32
hoelzl@57234
    33
theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
hoelzl@57234
    34
proof
hoelzl@57234
    35
  assume "\<exists>f::nat \<Rightarrow> real. surj f"
hoelzl@57234
    36
  then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
wenzelm@56796
    37
hoelzl@57234
    38
  txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *}
wenzelm@23461
    39
hoelzl@57234
    40
  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
    41
    using assms
hoelzl@57234
    42
    by (auto simp add: not_le cong: conj_cong)
hoelzl@57234
    43
       (metis dense le_less_linear less_linear less_trans order_refl)
hoelzl@57234
    44
  then obtain i j where ij:
hoelzl@57234
    45
    "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
hoelzl@57234
    46
    "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
hoelzl@57234
    47
    "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
hoelzl@57234
    48
    by metis
wenzelm@23461
    49
hoelzl@57234
    50
  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
    51
  def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
wenzelm@23461
    52
hoelzl@57234
    53
  have ivl[simp]:
hoelzl@57234
    54
    "ivl 0 = (f 0 + 1, f 0 + 2)"
hoelzl@57234
    55
    "\<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
    56
    unfolding ivl_def by simp_all
wenzelm@56796
    57
hoelzl@57234
    58
  txt {* This is a decreasing sequence of non-empty intervals. *}
wenzelm@23461
    59
hoelzl@57234
    60
  { fix n have "fst (ivl n) < snd (ivl n)"
hoelzl@57234
    61
      by (induct n) (auto intro!: ij) }
hoelzl@57234
    62
  note less = this
wenzelm@23461
    63
hoelzl@57234
    64
  have "decseq I"
hoelzl@57234
    65
    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
hoelzl@57234
    66
hoelzl@57234
    67
  txt {* Now we apply the finite intersection property of compact sets. *}
wenzelm@23461
    68
hoelzl@57234
    69
  have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
hoelzl@57234
    70
  proof (rule compact_imp_fip_image)
hoelzl@57234
    71
    fix S :: "nat set" assume fin: "finite S"
hoelzl@57234
    72
    have "{} \<subset> I (Max (insert 0 S))"
hoelzl@57234
    73
      unfolding I_def using less[of "Max (insert 0 S)"] by auto
hoelzl@57234
    74
    also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
hoelzl@57234
    75
      using fin decseqD[OF `decseq I`, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
hoelzl@57234
    76
    also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
wenzelm@56796
    77
      by auto
hoelzl@57234
    78
    finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
wenzelm@53372
    79
      by auto
hoelzl@57234
    80
  qed (auto simp: I_def)
hoelzl@57234
    81
  then obtain x where "\<And>n. x \<in> I n"
hoelzl@57234
    82
    by blast
hoelzl@57234
    83
  moreover from `surj f` obtain j where "x = f j"
hoelzl@57234
    84
    by blast
hoelzl@57234
    85
  ultimately have "f j \<in> I (Suc j)"
hoelzl@57234
    86
    by blast
hoelzl@57234
    87
  with ij(3)[OF less] show False
hoelzl@57234
    88
    unfolding I_def ivl fst_conv snd_conv by auto
wenzelm@23461
    89
qed
wenzelm@23461
    90
hoelzl@57234
    91
lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
hoelzl@57234
    92
  using real_non_denum unfolding uncountable_def by auto
wenzelm@23461
    93
hoelzl@57234
    94
lemma bij_betw_open_intervals:
hoelzl@57234
    95
  fixes a b c d :: real
hoelzl@57234
    96
  assumes "a < b" "c < d"
hoelzl@57234
    97
  shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
hoelzl@57234
    98
proof -
hoelzl@57234
    99
  def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
hoelzl@57234
   100
  { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
hoelzl@57234
   101
    moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
hoelzl@57234
   102
      by (intro mult_strict_left_mono) simp_all
hoelzl@57234
   103
    moreover from * have "0 < (d - c) * (x - a) / (b - a)"
hoelzl@57234
   104
      by simp
hoelzl@57234
   105
    ultimately have "f a b c d x < d" "c < f a b c d x"
hoelzl@57234
   106
      by (simp_all add: f_def field_simps) }
hoelzl@57234
   107
  with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
hoelzl@57234
   108
    by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
hoelzl@57234
   109
  thus ?thesis by auto
wenzelm@23461
   110
qed
wenzelm@23461
   111
hoelzl@57234
   112
lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
lp15@59872
   113
  using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
wenzelm@23461
   114
hoelzl@57234
   115
lemma uncountable_open_interval:
lp15@60308
   116
  fixes a b :: real 
lp15@60308
   117
  shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
lp15@60308
   118
proof
lp15@60308
   119
  assume "uncountable {a<..<b}"
lp15@60308
   120
  then show "a < b"
lp15@60308
   121
    using uncountable_def by force
lp15@60308
   122
next 
lp15@60308
   123
  assume "a < b"
lp15@60308
   124
  show "uncountable {a<..<b}"
lp15@60308
   125
  proof -
lp15@60308
   126
    obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
lp15@60308
   127
      using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
lp15@60308
   128
    then show ?thesis
lp15@60308
   129
      by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
lp15@60308
   130
  qed
wenzelm@23461
   131
qed
wenzelm@23461
   132
lp15@60308
   133
lemma uncountable_half_open_interval_1:
lp15@60308
   134
  fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
lp15@60308
   135
  apply auto
lp15@60308
   136
  using atLeastLessThan_empty_iff apply fastforce
lp15@60308
   137
  using uncountable_open_interval [of a b]
lp15@60308
   138
  by (metis countable_Un_iff ivl_disj_un_singleton(3))
lp15@60308
   139
lp15@60308
   140
lemma uncountable_half_open_interval_2:
lp15@60308
   141
  fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
lp15@60308
   142
  apply auto
lp15@60308
   143
  using atLeastLessThan_empty_iff apply fastforce
lp15@60308
   144
  using uncountable_open_interval [of a b]
lp15@60308
   145
  by (metis countable_Un_iff ivl_disj_un_singleton(4))
lp15@60308
   146
wenzelm@23461
   147
end