src/HOL/Library/ContNotDenum.thy
author wenzelm
Tue Apr 29 22:50:55 2014 +0200 (2014-04-29)
changeset 56796 9f84219715a7
parent 54797 be020ec8560c
child 57234 596a499318ab
permissions -rw-r--r--
tuned proofs;
wenzelm@56796
     1
(*  Title:      HOL/Library/ContNonDenum.thy
wenzelm@56796
     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@56796
    18
words, there does not exist a function @{text "f: \<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@56796
    28
last) is non-empty. We then assume a surjective function @{text
wenzelm@56796
    29
"f: \<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@56796
    32
wenzelm@23461
    33
subsection {* Closed Intervals *}
wenzelm@23461
    34
wenzelm@23461
    35
subsection {* Nested Interval Property *}
wenzelm@23461
    36
wenzelm@23461
    37
theorem NIP:
wenzelm@56796
    38
  fixes f :: "nat \<Rightarrow> real set"
wenzelm@23461
    39
  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
wenzelm@56796
    40
    and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
wenzelm@23461
    41
  shows "(\<Inter>n. f n) \<noteq> {}"
wenzelm@23461
    42
proof -
hoelzl@54797
    43
  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
wenzelm@56796
    44
  {
wenzelm@56796
    45
    fix n
hoelzl@54797
    46
    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
hoelzl@54797
    47
      by auto
hoelzl@54797
    48
    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
wenzelm@56796
    49
      by auto
wenzelm@56796
    50
  }
hoelzl@54797
    51
  note f_eq = this
wenzelm@56796
    52
  {
wenzelm@56796
    53
    fix n m :: nat
wenzelm@56796
    54
    assume "n \<le> m"
wenzelm@56796
    55
    then have "f m \<subseteq> f n"
wenzelm@56796
    56
      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
wenzelm@56796
    57
  }
hoelzl@54797
    58
  note subset' = this
wenzelm@23461
    59
hoelzl@54797
    60
  have "compact (f 0)"
hoelzl@54797
    61
    by (subst f_eq) (rule compact_Icc)
hoelzl@54797
    62
  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
hoelzl@54797
    63
  proof (rule compact_imp_fip_image)
wenzelm@56796
    64
    fix I :: "nat set"
wenzelm@56796
    65
    assume I: "finite I"
hoelzl@54797
    66
    have "{} \<subset> f (Max (insert 0 I))"
hoelzl@54797
    67
      using f_eq[of "Max (insert 0 I)"] by auto
hoelzl@54797
    68
    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
hoelzl@54797
    69
    proof (rule INF_greatest)
wenzelm@56796
    70
      fix i
wenzelm@56796
    71
      assume "i \<in> insert 0 I"
hoelzl@54797
    72
      with I show "f (Max (insert 0 I)) \<subseteq> f i"
hoelzl@54797
    73
        by (intro subset') auto
wenzelm@23461
    74
    qed
hoelzl@54797
    75
    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
hoelzl@54797
    76
      by auto
hoelzl@54797
    77
  qed (subst f_eq, auto)
hoelzl@54797
    78
  then show "(\<Inter>n. f n) \<noteq> {}"
hoelzl@54797
    79
    by auto
wenzelm@23461
    80
qed
wenzelm@23461
    81
wenzelm@56796
    82
wenzelm@23461
    83
subsection {* Generating the intervals *}
wenzelm@23461
    84
wenzelm@23461
    85
subsubsection {* Existence of non-singleton closed intervals *}
wenzelm@23461
    86
wenzelm@23461
    87
text {* This lemma asserts that given any non-singleton closed
wenzelm@23461
    88
interval (a,b) and any element c, there exists a closed interval that
wenzelm@23461
    89
is a subset of (a,b) and that does not contain c and is a
wenzelm@23461
    90
non-singleton itself. *}
wenzelm@23461
    91
wenzelm@23461
    92
lemma closed_subset_ex:
wenzelm@56796
    93
  fixes c :: real
wenzelm@53372
    94
  assumes "a < b"
hoelzl@54797
    95
  shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
wenzelm@53372
    96
proof (cases "c < b")
wenzelm@53372
    97
  case True
wenzelm@53372
    98
  show ?thesis
wenzelm@53372
    99
  proof (cases "c < a")
wenzelm@53372
   100
    case True
hoelzl@54797
   101
    with `a < b` `c < b` have "c \<notin> {a..b}"
hoelzl@54797
   102
      by auto
wenzelm@56796
   103
    with `a < b` show ?thesis
wenzelm@56796
   104
      by auto
wenzelm@53372
   105
  next
wenzelm@53372
   106
    case False
wenzelm@53372
   107
    then have "a \<le> c" by simp
wenzelm@53372
   108
    def ka \<equiv> "(c + b)/2"
wenzelm@56796
   109
    from ka_def `c < b` have "ka < b"
wenzelm@56796
   110
      by auto
wenzelm@56796
   111
    moreover from ka_def `c < b` have "ka > c"
wenzelm@56796
   112
      by simp
wenzelm@56796
   113
    ultimately have "c \<notin> {ka..b}"
wenzelm@56796
   114
      by auto
wenzelm@56796
   115
    moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
wenzelm@56796
   116
      by simp
wenzelm@56796
   117
    then have "{ka..b} \<subseteq> {a..b}"
wenzelm@56796
   118
      by auto
wenzelm@56796
   119
    ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
wenzelm@56796
   120
      using `ka < b` by auto
wenzelm@53372
   121
    then show ?thesis
wenzelm@53372
   122
      by auto
wenzelm@53372
   123
  qed
wenzelm@53372
   124
next
wenzelm@53372
   125
  case False
wenzelm@53372
   126
  then have "c \<ge> b" by simp
wenzelm@53372
   127
  def kb \<equiv> "(a + b)/2"
wenzelm@53372
   128
  with `a < b` have "kb < b" by auto
wenzelm@56796
   129
  with kb_def `c \<ge> b` have "a < kb" "kb < c"
wenzelm@56796
   130
    by auto
hoelzl@54797
   131
  from `kb < c` have c: "c \<notin> {a..kb}"
hoelzl@54797
   132
    by auto
hoelzl@54797
   133
  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
hoelzl@54797
   134
    by auto
hoelzl@54797
   135
  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
wenzelm@53372
   136
    by simp
wenzelm@56796
   137
  then show ?thesis
wenzelm@56796
   138
    by auto
wenzelm@23461
   139
qed
wenzelm@23461
   140
wenzelm@56796
   141
wenzelm@23461
   142
subsection {* newInt: Interval generation *}
wenzelm@23461
   143
wenzelm@23461
   144
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
wenzelm@23461
   145
closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
wenzelm@23461
   146
does not contain @{text "f (Suc n)"}. With the base case defined such
wenzelm@23461
   147
that @{text "(f 0)\<notin>newInt 0 f"}. *}
wenzelm@23461
   148
wenzelm@56796
   149
wenzelm@23461
   150
subsubsection {* Definition *}
wenzelm@23461
   151
wenzelm@56796
   152
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
wenzelm@56796
   153
where
hoelzl@54797
   154
  "newInt 0 f = {f 0 + 1..f 0 + 2}"
wenzelm@56796
   155
| "newInt (Suc n) f =
wenzelm@56796
   156
    (SOME e.
wenzelm@56796
   157
      (\<exists>e1 e2.
wenzelm@56796
   158
         e1 < e2 \<and>
wenzelm@56796
   159
         e = {e1..e2} \<and>
wenzelm@56796
   160
         e \<subseteq> newInt n f \<and>
wenzelm@56796
   161
         f (Suc n) \<notin> e))"
haftmann@27435
   162
wenzelm@23461
   163
wenzelm@23461
   164
subsubsection {* Properties *}
wenzelm@23461
   165
wenzelm@23461
   166
text {* We now show that every application of newInt returns an
wenzelm@23461
   167
appropriate interval. *}
wenzelm@23461
   168
wenzelm@23461
   169
lemma newInt_ex:
wenzelm@23461
   170
  "\<exists>a b. a < b \<and>
wenzelm@56796
   171
    newInt (Suc n) f = {a..b} \<and>
wenzelm@56796
   172
    newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@56796
   173
    f (Suc n) \<notin> newInt (Suc n) f"
wenzelm@23461
   174
proof (induct n)
wenzelm@23461
   175
  case 0
wenzelm@23461
   176
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@56796
   177
    e1 < e2 \<and>
wenzelm@56796
   178
    e = {e1..e2} \<and>
wenzelm@56796
   179
    e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
wenzelm@56796
   180
    f (Suc 0) \<notin> e"
wenzelm@23461
   181
wenzelm@23461
   182
  have "newInt (Suc 0) f = ?e" by auto
wenzelm@23461
   183
  moreover
wenzelm@23461
   184
  have "f 0 + 1 < f 0 + 2" by simp
wenzelm@56796
   185
  with closed_subset_ex
wenzelm@56796
   186
  have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
wenzelm@56796
   187
  then have "\<exists>e. \<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@56796
   188
    by simp
wenzelm@56796
   189
  then have "\<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
   190
    by (rule someI_ex)
wenzelm@23461
   191
  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
wenzelm@56796
   192
      newInt (Suc 0) f = {e1..e2} \<and>
wenzelm@56796
   193
      newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
wenzelm@56796
   194
      f (Suc 0) \<notin> newInt (Suc 0) f"
wenzelm@56796
   195
    by simp
wenzelm@56796
   196
  then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
wenzelm@56796
   197
      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
wenzelm@23461
   198
    by simp
wenzelm@23461
   199
next
wenzelm@23461
   200
  case (Suc n)
wenzelm@56796
   201
  then have "\<exists>a b.
wenzelm@56796
   202
      a < b \<and>
wenzelm@56796
   203
      newInt (Suc n) f = {a..b} \<and>
wenzelm@56796
   204
      newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@56796
   205
      f (Suc n) \<notin> newInt (Suc n) f"
wenzelm@56796
   206
    by simp
wenzelm@23461
   207
  then obtain a and b where ab: "a < b \<and>
wenzelm@56796
   208
      newInt (Suc n) f = {a..b} \<and>
wenzelm@56796
   209
      newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@56796
   210
      f (Suc n) \<notin> newInt (Suc n) f"
wenzelm@56796
   211
    by auto
wenzelm@56796
   212
  then have cab: "{a..b} = newInt (Suc n) f"
wenzelm@56796
   213
    by simp
wenzelm@23461
   214
wenzelm@23461
   215
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@56796
   216
      e1 < e2 \<and>
wenzelm@56796
   217
      e = {e1..e2} \<and>
wenzelm@56796
   218
      e \<subseteq> {a..b} \<and>
wenzelm@56796
   219
      f (Suc (Suc n)) \<notin> e"
wenzelm@56796
   220
  from cab have ni: "newInt (Suc (Suc n)) f = ?e"
wenzelm@56796
   221
    by auto
wenzelm@23461
   222
wenzelm@23461
   223
  from ab have "a < b" by simp
wenzelm@56796
   224
  with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
wenzelm@56796
   225
    f (Suc (Suc n)) \<notin> {ka..kb}" .
wenzelm@56796
   226
  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
wenzelm@56796
   227
      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
wenzelm@56796
   228
    by simp
wenzelm@56796
   229
  then have "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e"
wenzelm@23461
   230
    by simp
wenzelm@56796
   231
  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
wenzelm@56796
   232
    by (rule someI_ex)
wenzelm@56796
   233
  with ab ni show "\<exists>ka kb. ka < kb \<and>
wenzelm@56796
   234
      newInt (Suc (Suc n)) f = {ka..kb} \<and>
wenzelm@56796
   235
      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
wenzelm@56796
   236
      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
wenzelm@56796
   237
    by auto
wenzelm@23461
   238
qed
wenzelm@23461
   239
wenzelm@56796
   240
lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
wenzelm@23461
   241
  using newInt_ex by auto
wenzelm@23461
   242
wenzelm@23461
   243
wenzelm@23461
   244
text {* Another fundamental property is that no element in the range
wenzelm@23461
   245
of f is in the intersection of all closed intervals generated by
wenzelm@23461
   246
newInt. *}
wenzelm@23461
   247
wenzelm@56796
   248
lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
wenzelm@23461
   249
proof
wenzelm@56796
   250
  fix n :: nat
wenzelm@56796
   251
  have "f n \<notin> newInt n f"
wenzelm@56796
   252
  proof (cases n)
wenzelm@56796
   253
    case 0
wenzelm@56796
   254
    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
wenzelm@56796
   255
      by simp
wenzelm@56796
   256
    ultimately show ?thesis by simp
wenzelm@56796
   257
  next
wenzelm@56796
   258
    case (Suc m)
wenzelm@56796
   259
    from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
wenzelm@56796
   260
      newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
wenzelm@56796
   261
    then have "f (Suc m) \<notin> newInt (Suc m) f"
wenzelm@56796
   262
      by auto
wenzelm@56796
   263
    with Suc show ?thesis by simp
wenzelm@56796
   264
  qed
wenzelm@56796
   265
  then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
wenzelm@23461
   266
qed
wenzelm@23461
   267
wenzelm@56796
   268
lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
wenzelm@23461
   269
proof -
wenzelm@23461
   270
  let ?g = "\<lambda>n. newInt n f"
wenzelm@23461
   271
  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
wenzelm@23461
   272
  proof
wenzelm@23461
   273
    fix n
wenzelm@23461
   274
    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
wenzelm@23461
   275
  qed
hoelzl@54797
   276
  moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
wenzelm@23461
   277
  proof
wenzelm@56796
   278
    fix n :: nat
wenzelm@56796
   279
    show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
wenzelm@56796
   280
    proof (cases n)
wenzelm@56796
   281
      case 0
wenzelm@56796
   282
      then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
wenzelm@23461
   283
        by simp
wenzelm@56796
   284
      then show ?thesis
wenzelm@56796
   285
        by blast
wenzelm@56796
   286
    next
wenzelm@56796
   287
      case (Suc m)
wenzelm@56796
   288
      have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
wenzelm@23461
   289
        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
wenzelm@23461
   290
        by (rule newInt_ex)
wenzelm@56796
   291
      then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
wenzelm@56796
   292
        by auto
wenzelm@56796
   293
      with Suc have "?g n = {a..b} \<and> a \<le> b"
wenzelm@56796
   294
        by auto
wenzelm@56796
   295
      then show ?thesis
wenzelm@56796
   296
        by blast
wenzelm@56796
   297
    qed
wenzelm@23461
   298
  qed
wenzelm@23461
   299
  ultimately show ?thesis by (rule NIP)
wenzelm@23461
   300
qed
wenzelm@23461
   301
wenzelm@23461
   302
wenzelm@23461
   303
subsection {* Final Theorem *}
wenzelm@23461
   304
wenzelm@56796
   305
theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
wenzelm@56796
   306
proof
wenzelm@56796
   307
  assume "\<exists>f :: nat \<Rightarrow> real. surj f"
wenzelm@56796
   308
  then obtain f :: "nat \<Rightarrow> real" where "surj f"
wenzelm@56796
   309
    by auto
wenzelm@56796
   310
  txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
wenzelm@56796
   311
  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
wenzelm@56796
   312
    using newInt_notempty by blast
wenzelm@56796
   313
  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
wenzelm@56796
   314
    by (rule newInt_inter)
wenzelm@56796
   315
  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
wenzelm@56796
   316
    by blast
wenzelm@56796
   317
  moreover from `surj f` have "x \<in> range f"
wenzelm@56796
   318
    by simp
wenzelm@56796
   319
  ultimately show False
wenzelm@56796
   320
    by blast
wenzelm@23461
   321
qed
wenzelm@23461
   322
wenzelm@23461
   323
end
hoelzl@54797
   324