src/HOL/Library/ContNotDenum.thy
author hoelzl
Wed Dec 18 11:53:40 2013 +0100 (2013-12-18)
changeset 54797 be020ec8560c
parent 54263 c4159fe6fa46
child 56796 9f84219715a7
permissions -rw-r--r--
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
haftmann@28952
     1
(*  Title       : HOL/ContNonDenum
wenzelm@23461
     2
    Author      : Benjamin Porter, Monash University, NICTA, 2005
wenzelm@23461
     3
*)
wenzelm@23461
     4
wenzelm@23461
     5
header {* Non-denumerability of the Continuum. *}
wenzelm@23461
     6
wenzelm@23461
     7
theory ContNotDenum
haftmann@30663
     8
imports Complex_Main
wenzelm@23461
     9
begin
wenzelm@23461
    10
wenzelm@23461
    11
subsection {* Abstract *}
wenzelm@23461
    12
wenzelm@23461
    13
text {* The following document presents a proof that the Continuum is
wenzelm@23461
    14
uncountable. It is formalised in the Isabelle/Isar theorem proving
wenzelm@23461
    15
system.
wenzelm@23461
    16
wenzelm@23461
    17
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
wenzelm@23461
    18
words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
wenzelm@23461
    19
surjective.
wenzelm@23461
    20
wenzelm@23461
    21
{\em Outline:} An elegant informal proof of this result uses Cantor's
wenzelm@23461
    22
Diagonalisation argument. The proof presented here is not this
wenzelm@23461
    23
one. First we formalise some properties of closed intervals, then we
wenzelm@23461
    24
prove the Nested Interval Property. This property relies on the
wenzelm@23461
    25
completeness of the Real numbers and is the foundation for our
wenzelm@23461
    26
argument. Informally it states that an intersection of countable
wenzelm@23461
    27
closed intervals (where each successive interval is a subset of the
wenzelm@23461
    28
last) is non-empty. We then assume a surjective function f:@{text
wenzelm@23461
    29
"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
wenzelm@23461
    30
by generating a sequence of closed intervals then using the NIP. *}
wenzelm@23461
    31
wenzelm@23461
    32
subsection {* Closed Intervals *}
wenzelm@23461
    33
wenzelm@23461
    34
subsection {* Nested Interval Property *}
wenzelm@23461
    35
wenzelm@23461
    36
theorem NIP:
wenzelm@23461
    37
  fixes f::"nat \<Rightarrow> real set"
wenzelm@23461
    38
  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
hoelzl@54797
    39
  and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
wenzelm@23461
    40
  shows "(\<Inter>n. f n) \<noteq> {}"
wenzelm@23461
    41
proof -
hoelzl@54797
    42
  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
hoelzl@54797
    43
  { fix n 
hoelzl@54797
    44
    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
hoelzl@54797
    45
      by auto
hoelzl@54797
    46
    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
hoelzl@54797
    47
      by auto }
hoelzl@54797
    48
  note f_eq = this
hoelzl@54797
    49
  { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
hoelzl@54797
    50
      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
hoelzl@54797
    51
  note subset' = this
wenzelm@23461
    52
hoelzl@54797
    53
  have "compact (f 0)"
hoelzl@54797
    54
    by (subst f_eq) (rule compact_Icc)
hoelzl@54797
    55
  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
hoelzl@54797
    56
  proof (rule compact_imp_fip_image)
hoelzl@54797
    57
    fix I :: "nat set" assume I: "finite I"
hoelzl@54797
    58
    have "{} \<subset> f (Max (insert 0 I))"
hoelzl@54797
    59
      using f_eq[of "Max (insert 0 I)"] by auto
hoelzl@54797
    60
    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
hoelzl@54797
    61
    proof (rule INF_greatest)
hoelzl@54797
    62
      fix i assume "i \<in> insert 0 I"
hoelzl@54797
    63
      with I show "f (Max (insert 0 I)) \<subseteq> f i"
hoelzl@54797
    64
        by (intro subset') auto
wenzelm@23461
    65
    qed
hoelzl@54797
    66
    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
hoelzl@54797
    67
      by auto
hoelzl@54797
    68
  qed (subst f_eq, auto)
hoelzl@54797
    69
  then show "(\<Inter>n. f n) \<noteq> {}"
hoelzl@54797
    70
    by auto
wenzelm@23461
    71
qed
wenzelm@23461
    72
wenzelm@23461
    73
subsection {* Generating the intervals *}
wenzelm@23461
    74
wenzelm@23461
    75
subsubsection {* Existence of non-singleton closed intervals *}
wenzelm@23461
    76
wenzelm@23461
    77
text {* This lemma asserts that given any non-singleton closed
wenzelm@23461
    78
interval (a,b) and any element c, there exists a closed interval that
wenzelm@23461
    79
is a subset of (a,b) and that does not contain c and is a
wenzelm@23461
    80
non-singleton itself. *}
wenzelm@23461
    81
wenzelm@23461
    82
lemma closed_subset_ex:
wenzelm@23461
    83
  fixes c::real
wenzelm@53372
    84
  assumes "a < b"
hoelzl@54797
    85
  shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
wenzelm@53372
    86
proof (cases "c < b")
wenzelm@53372
    87
  case True
wenzelm@53372
    88
  show ?thesis
wenzelm@53372
    89
  proof (cases "c < a")
wenzelm@53372
    90
    case True
hoelzl@54797
    91
    with `a < b` `c < b` have "c \<notin> {a..b}"
hoelzl@54797
    92
      by auto
wenzelm@53372
    93
    with `a < b` show ?thesis by auto
wenzelm@53372
    94
  next
wenzelm@53372
    95
    case False
wenzelm@53372
    96
    then have "a \<le> c" by simp
wenzelm@53372
    97
    def ka \<equiv> "(c + b)/2"
wenzelm@23461
    98
wenzelm@53372
    99
    from ka_def `c < b` have kalb: "ka < b" by auto
wenzelm@53372
   100
    moreover from ka_def `c < b` have kagc: "ka > c" by simp
hoelzl@54797
   101
    ultimately have "c\<notin>{ka..b}" by auto
wenzelm@53372
   102
    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
hoelzl@54797
   103
    hence "{ka..b} \<subseteq> {a..b}" by auto
wenzelm@23461
   104
    ultimately have
hoelzl@54797
   105
      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
wenzelm@53372
   106
      using kalb by auto
wenzelm@53372
   107
    then show ?thesis
wenzelm@53372
   108
      by auto
wenzelm@53372
   109
  qed
wenzelm@53372
   110
next
wenzelm@53372
   111
  case False
wenzelm@53372
   112
  then have "c \<ge> b" by simp
wenzelm@23461
   113
wenzelm@53372
   114
  def kb \<equiv> "(a + b)/2"
wenzelm@53372
   115
  with `a < b` have "kb < b" by auto
wenzelm@53372
   116
  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
hoelzl@54797
   117
  from `kb < c` have c: "c \<notin> {a..kb}"
hoelzl@54797
   118
    by auto
hoelzl@54797
   119
  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
hoelzl@54797
   120
    by auto
hoelzl@54797
   121
  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
wenzelm@53372
   122
    by simp
wenzelm@53372
   123
  then show ?thesis by auto
wenzelm@23461
   124
qed
wenzelm@23461
   125
wenzelm@23461
   126
subsection {* newInt: Interval generation *}
wenzelm@23461
   127
wenzelm@23461
   128
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
wenzelm@23461
   129
closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
wenzelm@23461
   130
does not contain @{text "f (Suc n)"}. With the base case defined such
wenzelm@23461
   131
that @{text "(f 0)\<notin>newInt 0 f"}. *}
wenzelm@23461
   132
wenzelm@23461
   133
subsubsection {* Definition *}
wenzelm@23461
   134
haftmann@27435
   135
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
hoelzl@54797
   136
  "newInt 0 f = {f 0 + 1..f 0 + 2}"
haftmann@27435
   137
  | "newInt (Suc n) f =
haftmann@27435
   138
      (SOME e. (\<exists>e1 e2.
haftmann@27435
   139
       e1 < e2 \<and>
hoelzl@54797
   140
       e = {e1..e2} \<and>
hoelzl@54797
   141
       e \<subseteq> newInt n f \<and>
hoelzl@54797
   142
       f (Suc n) \<notin> e)
haftmann@27435
   143
      )"
haftmann@27435
   144
wenzelm@23461
   145
wenzelm@23461
   146
subsubsection {* Properties *}
wenzelm@23461
   147
wenzelm@23461
   148
text {* We now show that every application of newInt returns an
wenzelm@23461
   149
appropriate interval. *}
wenzelm@23461
   150
wenzelm@23461
   151
lemma newInt_ex:
wenzelm@23461
   152
  "\<exists>a b. a < b \<and>
hoelzl@54797
   153
   newInt (Suc n) f = {a..b} \<and>
wenzelm@23461
   154
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   155
   f (Suc n) \<notin> newInt (Suc n) f"
wenzelm@23461
   156
proof (induct n)
wenzelm@23461
   157
  case 0
wenzelm@23461
   158
wenzelm@23461
   159
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@23461
   160
   e1 < e2 \<and>
hoelzl@54797
   161
   e = {e1..e2} \<and>
hoelzl@54797
   162
   e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
wenzelm@23461
   163
   f (Suc 0) \<notin> e"
wenzelm@23461
   164
wenzelm@23461
   165
  have "newInt (Suc 0) f = ?e" by auto
wenzelm@23461
   166
  moreover
wenzelm@23461
   167
  have "f 0 + 1 < f 0 + 2" by simp
wenzelm@23461
   168
  with closed_subset_ex have
hoelzl@54797
   169
    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
hoelzl@54797
   170
     f (Suc 0) \<notin> {ka..kb}" .
wenzelm@23461
   171
  hence
hoelzl@54797
   172
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
hoelzl@54797
   173
     e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
wenzelm@23461
   174
  hence
hoelzl@54797
   175
    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
wenzelm@23461
   176
    by (rule someI_ex)
wenzelm@23461
   177
  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
hoelzl@54797
   178
   newInt (Suc 0) f = {e1..e2} \<and>
hoelzl@54797
   179
   newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
wenzelm@23461
   180
   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
wenzelm@23461
   181
  thus
hoelzl@54797
   182
    "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
wenzelm@23461
   183
     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
wenzelm@23461
   184
    by simp
wenzelm@23461
   185
next
wenzelm@23461
   186
  case (Suc n)
wenzelm@23461
   187
  hence "\<exists>a b.
wenzelm@23461
   188
   a < b \<and>
hoelzl@54797
   189
   newInt (Suc n) f = {a..b} \<and>
wenzelm@23461
   190
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   191
   f (Suc n) \<notin> newInt (Suc n) f" by simp
wenzelm@23461
   192
  then obtain a and b where ab: "a < b \<and>
hoelzl@54797
   193
   newInt (Suc n) f = {a..b} \<and>
wenzelm@23461
   194
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   195
   f (Suc n) \<notin> newInt (Suc n) f" by auto
hoelzl@54797
   196
  hence cab: "{a..b} = newInt (Suc n) f" by simp
wenzelm@23461
   197
wenzelm@23461
   198
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@23461
   199
    e1 < e2 \<and>
hoelzl@54797
   200
    e = {e1..e2} \<and>
hoelzl@54797
   201
    e \<subseteq> {a..b} \<and>
wenzelm@23461
   202
    f (Suc (Suc n)) \<notin> e"
wenzelm@23461
   203
  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
wenzelm@23461
   204
wenzelm@23461
   205
  from ab have "a < b" by simp
wenzelm@23461
   206
  with closed_subset_ex have
hoelzl@54797
   207
    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
hoelzl@54797
   208
     f (Suc (Suc n)) \<notin> {ka..kb}" .
wenzelm@23461
   209
  hence
hoelzl@54797
   210
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
hoelzl@54797
   211
     {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
wenzelm@23461
   212
    by simp
wenzelm@23461
   213
  hence
hoelzl@54797
   214
    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
hoelzl@54797
   215
     e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
wenzelm@23461
   216
  hence
hoelzl@54797
   217
    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
hoelzl@54797
   218
     ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
wenzelm@23461
   219
  with ab ni show
wenzelm@23461
   220
    "\<exists>ka kb. ka < kb \<and>
hoelzl@54797
   221
     newInt (Suc (Suc n)) f = {ka..kb} \<and>
wenzelm@23461
   222
     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
wenzelm@23461
   223
     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
wenzelm@23461
   224
qed
wenzelm@23461
   225
wenzelm@23461
   226
lemma newInt_subset:
wenzelm@23461
   227
  "newInt (Suc n) f \<subseteq> newInt n f"
wenzelm@23461
   228
  using newInt_ex by auto
wenzelm@23461
   229
wenzelm@23461
   230
wenzelm@23461
   231
text {* Another fundamental property is that no element in the range
wenzelm@23461
   232
of f is in the intersection of all closed intervals generated by
wenzelm@23461
   233
newInt. *}
wenzelm@23461
   234
wenzelm@23461
   235
lemma newInt_inter:
wenzelm@23461
   236
  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
wenzelm@23461
   237
proof
wenzelm@23461
   238
  fix n::nat
wenzelm@23461
   239
  {
wenzelm@23461
   240
    assume n0: "n = 0"
hoelzl@54797
   241
    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
hoelzl@54797
   242
    ultimately have "f n \<notin> newInt n f" by simp
wenzelm@23461
   243
  }
wenzelm@23461
   244
  moreover
wenzelm@23461
   245
  {
wenzelm@23461
   246
    assume "\<not> n = 0"
wenzelm@23461
   247
    hence "n > 0" by simp
wenzelm@23461
   248
    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm@23461
   249
wenzelm@23461
   250
    from newInt_ex have
hoelzl@54797
   251
      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
wenzelm@23461
   252
       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
wenzelm@23461
   253
    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
wenzelm@23461
   254
    with ndef have "f n \<notin> newInt n f" by simp
wenzelm@23461
   255
  }
wenzelm@23461
   256
  ultimately have "f n \<notin> newInt n f" by (rule case_split)
wenzelm@23461
   257
  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
wenzelm@23461
   258
qed
wenzelm@23461
   259
wenzelm@23461
   260
wenzelm@23461
   261
lemma newInt_notempty:
wenzelm@23461
   262
  "(\<Inter>n. newInt n f) \<noteq> {}"
wenzelm@23461
   263
proof -
wenzelm@23461
   264
  let ?g = "\<lambda>n. newInt n f"
wenzelm@23461
   265
  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
wenzelm@23461
   266
  proof
wenzelm@23461
   267
    fix n
wenzelm@23461
   268
    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
wenzelm@23461
   269
  qed
hoelzl@54797
   270
  moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
wenzelm@23461
   271
  proof
wenzelm@23461
   272
    fix n::nat
wenzelm@23461
   273
    {
wenzelm@23461
   274
      assume "n = 0"
wenzelm@23461
   275
      then have
hoelzl@54797
   276
        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
wenzelm@23461
   277
        by simp
hoelzl@54797
   278
      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
wenzelm@23461
   279
    }
wenzelm@23461
   280
    moreover
wenzelm@23461
   281
    {
wenzelm@23461
   282
      assume "\<not> n = 0"
wenzelm@23461
   283
      then have "n > 0" by simp
wenzelm@23461
   284
      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm@23461
   285
wenzelm@23461
   286
      have
hoelzl@54797
   287
        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
wenzelm@23461
   288
        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
wenzelm@23461
   289
        by (rule newInt_ex)
wenzelm@23461
   290
      then obtain a and b where
hoelzl@54797
   291
        "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
hoelzl@54797
   292
      with nd have "?g n = {a..b} \<and> a \<le> b" by auto
hoelzl@54797
   293
      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
wenzelm@23461
   294
    }
hoelzl@54797
   295
    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
wenzelm@23461
   296
  qed
wenzelm@23461
   297
  ultimately show ?thesis by (rule NIP)
wenzelm@23461
   298
qed
wenzelm@23461
   299
wenzelm@23461
   300
wenzelm@23461
   301
subsection {* Final Theorem *}
wenzelm@23461
   302
wenzelm@23461
   303
theorem real_non_denum:
wenzelm@23461
   304
  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
wenzelm@23461
   305
proof -- "by contradiction"
wenzelm@23461
   306
  assume "\<exists>f::nat\<Rightarrow>real. surj f"
hoelzl@40702
   307
  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
wenzelm@23461
   308
  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
wenzelm@23461
   309
  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
wenzelm@23461
   310
  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
wenzelm@23461
   311
  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
wenzelm@23461
   312
  moreover from rangeF have "x \<in> range f" by simp
wenzelm@23461
   313
  ultimately show False by blast
wenzelm@23461
   314
qed
wenzelm@23461
   315
wenzelm@23461
   316
end
hoelzl@54797
   317