src/HOL/Library/ContNotDenum.thy
author hoelzl
Tue Nov 05 09:45:02 2013 +0100 (2013-11-05)
changeset 54263 c4159fe6fa46
parent 53372 f5a6313c7fe4
child 54797 be020ec8560c
permissions -rw-r--r--
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
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
text {* This section formalises some properties of closed intervals. *}
wenzelm@23461
    35
wenzelm@23461
    36
subsubsection {* Definition *}
wenzelm@23461
    37
wenzelm@23461
    38
definition
wenzelm@23461
    39
  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
wenzelm@23461
    40
  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
wenzelm@23461
    41
wenzelm@23461
    42
subsubsection {* Properties *}
wenzelm@23461
    43
wenzelm@23461
    44
lemma closed_int_subset:
wenzelm@23461
    45
  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
wenzelm@23461
    46
  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
wenzelm@23461
    47
proof -
wenzelm@23461
    48
  {
wenzelm@23461
    49
    fix x::real
wenzelm@23461
    50
    assume "x \<in> closed_int x1 y1"
wenzelm@23461
    51
    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
wenzelm@23461
    52
    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
wenzelm@23461
    53
    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
wenzelm@23461
    54
  }
wenzelm@23461
    55
  thus ?thesis by auto
wenzelm@23461
    56
qed
wenzelm@23461
    57
wenzelm@23461
    58
lemma closed_int_least:
wenzelm@23461
    59
  assumes a: "a \<le> b"
wenzelm@23461
    60
  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
wenzelm@23461
    61
proof
wenzelm@23461
    62
  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
wenzelm@23461
    63
  thus "a \<in> closed_int a b" by (unfold closed_int_def)
wenzelm@23461
    64
next
wenzelm@23461
    65
  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
wenzelm@23461
    66
  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
wenzelm@23461
    67
qed
wenzelm@23461
    68
wenzelm@23461
    69
lemma closed_int_most:
wenzelm@23461
    70
  assumes a: "a \<le> b"
wenzelm@23461
    71
  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
wenzelm@23461
    72
proof
wenzelm@23461
    73
  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
wenzelm@23461
    74
  thus "b \<in> closed_int a b" by (unfold closed_int_def)
wenzelm@23461
    75
next
wenzelm@23461
    76
  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
wenzelm@23461
    77
  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
wenzelm@23461
    78
qed
wenzelm@23461
    79
wenzelm@23461
    80
lemma closed_not_empty:
wenzelm@23461
    81
  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 
wenzelm@23461
    82
  by (auto dest: closed_int_least)
wenzelm@23461
    83
wenzelm@23461
    84
lemma closed_mem:
wenzelm@23461
    85
  assumes "a \<le> c" and "c \<le> b"
wenzelm@23461
    86
  shows "c \<in> closed_int a b"
wenzelm@23461
    87
  using assms unfolding closed_int_def by auto
wenzelm@23461
    88
wenzelm@23461
    89
lemma closed_subset:
wenzelm@23461
    90
  assumes ac: "a \<le> b"  "c \<le> d" 
wenzelm@23461
    91
  assumes closed: "closed_int a b \<subseteq> closed_int c d"
wenzelm@23461
    92
  shows "b \<ge> c"
wenzelm@23461
    93
proof -
wenzelm@23461
    94
  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
wenzelm@23461
    95
  hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
wenzelm@23461
    96
  with ac have "c\<le>b \<and> b\<le>d" by simp
wenzelm@23461
    97
  thus ?thesis by auto
wenzelm@23461
    98
qed
wenzelm@23461
    99
wenzelm@23461
   100
wenzelm@23461
   101
subsection {* Nested Interval Property *}
wenzelm@23461
   102
wenzelm@23461
   103
theorem NIP:
wenzelm@23461
   104
  fixes f::"nat \<Rightarrow> real set"
wenzelm@23461
   105
  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
wenzelm@23461
   106
  and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
wenzelm@23461
   107
  shows "(\<Inter>n. f n) \<noteq> {}"
wenzelm@23461
   108
proof -
wenzelm@23461
   109
  let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
wenzelm@23461
   110
  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
wenzelm@23461
   111
  proof
wenzelm@23461
   112
    fix n
wenzelm@23461
   113
    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
wenzelm@23461
   114
    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
wenzelm@23461
   115
    hence "a \<le> b" ..
wenzelm@23461
   116
    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
wenzelm@23461
   117
    with fn show "\<exists>x. x\<in>(f n)" by simp
wenzelm@23461
   118
  qed
wenzelm@23461
   119
wenzelm@23461
   120
  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
wenzelm@23461
   121
  proof
wenzelm@23461
   122
    fix n
wenzelm@23461
   123
    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
wenzelm@23461
   124
    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
wenzelm@23461
   125
    hence "a \<le> b" by simp
wenzelm@23461
   126
    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
wenzelm@23461
   127
    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
wenzelm@23461
   128
    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
wenzelm@23461
   129
    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
wenzelm@23461
   130
  qed
wenzelm@23461
   131
wenzelm@23461
   132
  -- "A denotes the set of all left-most points of all the intervals ..."
wenzelm@23461
   133
  moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
hoelzl@54263
   134
  ultimately have "A \<noteq> {}"
wenzelm@23461
   135
  proof -
wenzelm@23461
   136
    have "(0::nat) \<in> \<nat>" by simp
hoelzl@54263
   137
    with Adef show ?thesis
hoelzl@54263
   138
      by blast
wenzelm@23461
   139
  qed
wenzelm@23461
   140
wenzelm@23461
   141
  -- "Now show that A is bounded above ..."
hoelzl@54263
   142
  moreover have "bdd_above A"
wenzelm@23461
   143
  proof -
wenzelm@23461
   144
    {
wenzelm@23461
   145
      fix n
wenzelm@23461
   146
      from ne have ex: "\<exists>x. x\<in>(f n)" ..
wenzelm@23461
   147
      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
wenzelm@23461
   148
      moreover
wenzelm@23461
   149
      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
wenzelm@23461
   150
      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
wenzelm@23461
   151
      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
wenzelm@23461
   152
      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
wenzelm@23461
   153
      with ex have "(?g n) \<le> b" by auto
wenzelm@23461
   154
      hence "\<exists>b. (?g n) \<le> b" by auto
wenzelm@23461
   155
    }
wenzelm@23461
   156
    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
wenzelm@23461
   157
wenzelm@23461
   158
    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
wenzelm@23461
   159
    proof (rule allI, induct_tac n)
wenzelm@23461
   160
      show "f 0 \<subseteq> f 0" by simp
wenzelm@23461
   161
    next
wenzelm@23461
   162
      fix n
wenzelm@23461
   163
      assume "f n \<subseteq> f 0"
wenzelm@23461
   164
      moreover from subset have "f (Suc n) \<subseteq> f n" ..
wenzelm@23461
   165
      ultimately show "f (Suc n) \<subseteq> f 0" by simp
wenzelm@23461
   166
    qed
wenzelm@23461
   167
    have "\<forall>n. (?g n)\<in>(f 0)"
wenzelm@23461
   168
    proof
wenzelm@23461
   169
      fix n
wenzelm@23461
   170
      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
wenzelm@23461
   171
      hence "?g n \<in> f n" ..
wenzelm@23461
   172
      with fs show "?g n \<in> f 0" by auto
wenzelm@23461
   173
    qed
wenzelm@23461
   174
    moreover from closed
wenzelm@23461
   175
      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
wenzelm@23461
   176
    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
wenzelm@23461
   177
    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
hoelzl@54263
   178
    with Adef show "bdd_above A" by auto
wenzelm@23461
   179
  qed
wenzelm@23461
   180
wenzelm@23461
   181
  -- "denote this least upper bound as t ..."
hoelzl@54263
   182
  def tdef: t == "Sup A"
wenzelm@23461
   183
wenzelm@23461
   184
  -- "and finally show that this least upper bound is in all the intervals..."
wenzelm@23461
   185
  have "\<forall>n. t \<in> f n"
wenzelm@23461
   186
  proof
wenzelm@23461
   187
    fix n::nat
wenzelm@23461
   188
    from closed obtain a and b where
wenzelm@23461
   189
      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
wenzelm@23461
   190
wenzelm@23461
   191
    have "t \<ge> a"
wenzelm@23461
   192
    proof -
wenzelm@23461
   193
      have "a \<in> A"
wenzelm@23461
   194
      proof -
wenzelm@23461
   195
          (* by construction *)
wenzelm@23461
   196
        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
wenzelm@23461
   197
          using closed_int_least by blast
wenzelm@23461
   198
        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
wenzelm@23461
   199
        proof clarsimp
wenzelm@23461
   200
          fix e
wenzelm@23461
   201
          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
wenzelm@23461
   202
          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
wenzelm@23461
   203
  
wenzelm@23461
   204
          from ein aux have "a \<le> e \<and> e \<le> e" by auto
wenzelm@23461
   205
          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
wenzelm@23461
   206
          ultimately show "e = a" by simp
wenzelm@23461
   207
        qed
wenzelm@23461
   208
        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
wenzelm@23461
   209
        ultimately have "(?g n) = a" by (rule some_equality)
wenzelm@23461
   210
        moreover
wenzelm@23461
   211
        {
wenzelm@23461
   212
          have "n = of_nat n" by simp
wenzelm@23461
   213
          moreover have "of_nat n \<in> \<nat>" by simp
wenzelm@23461
   214
          ultimately have "n \<in> \<nat>"
wenzelm@23461
   215
            apply -
wenzelm@23461
   216
            apply (subst(asm) eq_sym_conv)
wenzelm@23461
   217
            apply (erule subst)
wenzelm@23461
   218
            .
wenzelm@23461
   219
        }
wenzelm@23461
   220
        with Adef have "(?g n) \<in> A" by auto
wenzelm@23461
   221
        ultimately show ?thesis by simp
wenzelm@23461
   222
      qed 
hoelzl@54263
   223
      with `bdd_above A` show "a \<le> t"
hoelzl@54263
   224
        unfolding tdef by (intro cSup_upper)
wenzelm@23461
   225
    qed
wenzelm@23461
   226
    moreover have "t \<le> b"
hoelzl@54263
   227
      unfolding tdef
hoelzl@54263
   228
    proof (rule cSup_least)
hoelzl@54263
   229
      {
hoelzl@54263
   230
        from alb int have
hoelzl@54263
   231
          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
hoelzl@54263
   232
        
hoelzl@54263
   233
        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
hoelzl@54263
   234
        proof (rule allI, induct_tac m)
hoelzl@54263
   235
          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
hoelzl@54263
   236
        next
hoelzl@54263
   237
          fix m n
hoelzl@54263
   238
          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
wenzelm@23461
   239
          {
hoelzl@54263
   240
            fix p
hoelzl@54263
   241
            from pp have "f (p + n) \<subseteq> f p" by simp
hoelzl@54263
   242
            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
hoelzl@54263
   243
            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
hoelzl@54263
   244
            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
wenzelm@23461
   245
          }
hoelzl@54263
   246
          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
hoelzl@54263
   247
        qed 
hoelzl@54263
   248
        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
hoelzl@54263
   249
        proof ((rule allI)+, rule impI)
hoelzl@54263
   250
          fix \<alpha>::nat and \<beta>::nat
hoelzl@54263
   251
          assume "\<beta> \<le> \<alpha>"
hoelzl@54263
   252
          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
hoelzl@54263
   253
          then obtain k where "\<alpha> = \<beta> + k" ..
hoelzl@54263
   254
          moreover
hoelzl@54263
   255
          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
hoelzl@54263
   256
          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
hoelzl@54263
   257
        qed 
hoelzl@54263
   258
        
hoelzl@54263
   259
        fix m   
hoelzl@54263
   260
        {
hoelzl@54263
   261
          assume "m \<ge> n"
hoelzl@54263
   262
          with subsetm have "f m \<subseteq> f n" by simp
hoelzl@54263
   263
          with ain have "\<forall>x\<in>f m. x \<le> b" by auto
wenzelm@23461
   264
          moreover
hoelzl@54263
   265
          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
hoelzl@54263
   266
          ultimately have "?g m \<le> b" by auto
wenzelm@23461
   267
        }
hoelzl@54263
   268
        moreover
hoelzl@54263
   269
        {
hoelzl@54263
   270
          assume "\<not>(m \<ge> n)"
hoelzl@54263
   271
          hence "m < n" by simp
hoelzl@54263
   272
          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
hoelzl@54263
   273
          from closed obtain ma and mb where
hoelzl@54263
   274
            "f m = closed_int ma mb \<and> ma \<le> mb" by blast
hoelzl@54263
   275
          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
hoelzl@54263
   276
          from one alb sub fm int have "ma \<le> b" using closed_subset by blast
hoelzl@54263
   277
          moreover have "(?g m) = ma"
hoelzl@54263
   278
          proof -
hoelzl@54263
   279
            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
hoelzl@54263
   280
            moreover from one have
hoelzl@54263
   281
              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
hoelzl@54263
   282
              by (rule closed_int_least)
hoelzl@54263
   283
            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
hoelzl@54263
   284
            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
hoelzl@54263
   285
            thus "?g m = ma" by auto
hoelzl@54263
   286
          qed
hoelzl@54263
   287
          ultimately have "?g m \<le> b" by simp
hoelzl@54263
   288
        } 
hoelzl@54263
   289
        ultimately have "?g m \<le> b" by (rule case_split)
hoelzl@54263
   290
      }
hoelzl@54263
   291
      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
hoelzl@54263
   292
    qed fact
wenzelm@23461
   293
    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
wenzelm@23461
   294
    with int show "t \<in> f n" by simp
wenzelm@23461
   295
  qed
wenzelm@23461
   296
  hence "t \<in> (\<Inter>n. f n)" by auto
wenzelm@23461
   297
  thus ?thesis by auto
wenzelm@23461
   298
qed
wenzelm@23461
   299
wenzelm@23461
   300
subsection {* Generating the intervals *}
wenzelm@23461
   301
wenzelm@23461
   302
subsubsection {* Existence of non-singleton closed intervals *}
wenzelm@23461
   303
wenzelm@23461
   304
text {* This lemma asserts that given any non-singleton closed
wenzelm@23461
   305
interval (a,b) and any element c, there exists a closed interval that
wenzelm@23461
   306
is a subset of (a,b) and that does not contain c and is a
wenzelm@23461
   307
non-singleton itself. *}
wenzelm@23461
   308
wenzelm@23461
   309
lemma closed_subset_ex:
wenzelm@23461
   310
  fixes c::real
wenzelm@53372
   311
  assumes "a < b"
wenzelm@53372
   312
  shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
wenzelm@53372
   313
proof (cases "c < b")
wenzelm@53372
   314
  case True
wenzelm@53372
   315
  show ?thesis
wenzelm@53372
   316
  proof (cases "c < a")
wenzelm@53372
   317
    case True
wenzelm@53372
   318
    with `a < b` `c < b` have "c \<notin> closed_int a b"
wenzelm@53372
   319
      unfolding closed_int_def by auto
wenzelm@53372
   320
    with `a < b` show ?thesis by auto
wenzelm@53372
   321
  next
wenzelm@53372
   322
    case False
wenzelm@53372
   323
    then have "a \<le> c" by simp
wenzelm@53372
   324
    def ka \<equiv> "(c + b)/2"
wenzelm@23461
   325
wenzelm@53372
   326
    from ka_def `c < b` have kalb: "ka < b" by auto
wenzelm@53372
   327
    moreover from ka_def `c < b` have kagc: "ka > c" by simp
wenzelm@53372
   328
    ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
wenzelm@53372
   329
    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
wenzelm@53372
   330
    hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
wenzelm@23461
   331
    ultimately have
wenzelm@53372
   332
      "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
wenzelm@53372
   333
      using kalb by auto
wenzelm@53372
   334
    then show ?thesis
wenzelm@53372
   335
      by auto
wenzelm@53372
   336
  qed
wenzelm@53372
   337
next
wenzelm@53372
   338
  case False
wenzelm@53372
   339
  then have "c \<ge> b" by simp
wenzelm@23461
   340
wenzelm@53372
   341
  def kb \<equiv> "(a + b)/2"
wenzelm@53372
   342
  with `a < b` have "kb < b" by auto
wenzelm@53372
   343
  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
wenzelm@53372
   344
  from `kb < c` have c: "c \<notin> closed_int a kb"
wenzelm@53372
   345
    unfolding closed_int_def by auto
wenzelm@53372
   346
  with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
wenzelm@53372
   347
    unfolding closed_int_def by auto
wenzelm@53372
   348
  with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
wenzelm@53372
   349
    by simp
wenzelm@53372
   350
  then show ?thesis by auto
wenzelm@23461
   351
qed
wenzelm@23461
   352
wenzelm@23461
   353
subsection {* newInt: Interval generation *}
wenzelm@23461
   354
wenzelm@23461
   355
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
wenzelm@23461
   356
closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
wenzelm@23461
   357
does not contain @{text "f (Suc n)"}. With the base case defined such
wenzelm@23461
   358
that @{text "(f 0)\<notin>newInt 0 f"}. *}
wenzelm@23461
   359
wenzelm@23461
   360
subsubsection {* Definition *}
wenzelm@23461
   361
haftmann@27435
   362
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
haftmann@27435
   363
  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
haftmann@27435
   364
  | "newInt (Suc n) f =
haftmann@27435
   365
      (SOME e. (\<exists>e1 e2.
haftmann@27435
   366
       e1 < e2 \<and>
haftmann@27435
   367
       e = closed_int e1 e2 \<and>
haftmann@27435
   368
       e \<subseteq> (newInt n f) \<and>
haftmann@27435
   369
       (f (Suc n)) \<notin> e)
haftmann@27435
   370
      )"
haftmann@27435
   371
wenzelm@23461
   372
wenzelm@23461
   373
subsubsection {* Properties *}
wenzelm@23461
   374
wenzelm@23461
   375
text {* We now show that every application of newInt returns an
wenzelm@23461
   376
appropriate interval. *}
wenzelm@23461
   377
wenzelm@23461
   378
lemma newInt_ex:
wenzelm@23461
   379
  "\<exists>a b. a < b \<and>
wenzelm@23461
   380
   newInt (Suc n) f = closed_int a b \<and>
wenzelm@23461
   381
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   382
   f (Suc n) \<notin> newInt (Suc n) f"
wenzelm@23461
   383
proof (induct n)
wenzelm@23461
   384
  case 0
wenzelm@23461
   385
wenzelm@23461
   386
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@23461
   387
   e1 < e2 \<and>
wenzelm@23461
   388
   e = closed_int e1 e2 \<and>
wenzelm@23461
   389
   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
wenzelm@23461
   390
   f (Suc 0) \<notin> e"
wenzelm@23461
   391
wenzelm@23461
   392
  have "newInt (Suc 0) f = ?e" by auto
wenzelm@23461
   393
  moreover
wenzelm@23461
   394
  have "f 0 + 1 < f 0 + 2" by simp
wenzelm@23461
   395
  with closed_subset_ex have
wenzelm@23461
   396
    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
wenzelm@23461
   397
     f (Suc 0) \<notin> (closed_int ka kb)" .
wenzelm@23461
   398
  hence
wenzelm@23461
   399
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
wenzelm@23461
   400
     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
wenzelm@23461
   401
  hence
wenzelm@23461
   402
    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
wenzelm@23461
   403
     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
wenzelm@23461
   404
    by (rule someI_ex)
wenzelm@23461
   405
  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
wenzelm@23461
   406
   newInt (Suc 0) f = closed_int e1 e2 \<and>
wenzelm@23461
   407
   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
wenzelm@23461
   408
   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
wenzelm@23461
   409
  thus
wenzelm@23461
   410
    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
wenzelm@23461
   411
     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
wenzelm@23461
   412
    by simp
wenzelm@23461
   413
next
wenzelm@23461
   414
  case (Suc n)
wenzelm@23461
   415
  hence "\<exists>a b.
wenzelm@23461
   416
   a < b \<and>
wenzelm@23461
   417
   newInt (Suc n) f = closed_int a b \<and>
wenzelm@23461
   418
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   419
   f (Suc n) \<notin> newInt (Suc n) f" by simp
wenzelm@23461
   420
  then obtain a and b where ab: "a < b \<and>
wenzelm@23461
   421
   newInt (Suc n) f = closed_int a b \<and>
wenzelm@23461
   422
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   423
   f (Suc n) \<notin> newInt (Suc n) f" by auto
wenzelm@23461
   424
  hence cab: "closed_int a b = newInt (Suc n) f" by simp
wenzelm@23461
   425
wenzelm@23461
   426
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@23461
   427
    e1 < e2 \<and>
wenzelm@23461
   428
    e = closed_int e1 e2 \<and>
wenzelm@23461
   429
    e \<subseteq> closed_int a b \<and>
wenzelm@23461
   430
    f (Suc (Suc n)) \<notin> e"
wenzelm@23461
   431
  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
wenzelm@23461
   432
wenzelm@23461
   433
  from ab have "a < b" by simp
wenzelm@23461
   434
  with closed_subset_ex have
wenzelm@23461
   435
    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
wenzelm@23461
   436
     f (Suc (Suc n)) \<notin> closed_int ka kb" .
wenzelm@23461
   437
  hence
wenzelm@23461
   438
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
wenzelm@23461
   439
     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
wenzelm@23461
   440
    by simp
wenzelm@23461
   441
  hence
wenzelm@23461
   442
    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
wenzelm@23461
   443
     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
wenzelm@23461
   444
  hence
wenzelm@23461
   445
    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
wenzelm@23461
   446
     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
wenzelm@23461
   447
  with ab ni show
wenzelm@23461
   448
    "\<exists>ka kb. ka < kb \<and>
wenzelm@23461
   449
     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
wenzelm@23461
   450
     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
wenzelm@23461
   451
     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
wenzelm@23461
   452
qed
wenzelm@23461
   453
wenzelm@23461
   454
lemma newInt_subset:
wenzelm@23461
   455
  "newInt (Suc n) f \<subseteq> newInt n f"
wenzelm@23461
   456
  using newInt_ex by auto
wenzelm@23461
   457
wenzelm@23461
   458
wenzelm@23461
   459
text {* Another fundamental property is that no element in the range
wenzelm@23461
   460
of f is in the intersection of all closed intervals generated by
wenzelm@23461
   461
newInt. *}
wenzelm@23461
   462
wenzelm@23461
   463
lemma newInt_inter:
wenzelm@23461
   464
  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
wenzelm@23461
   465
proof
wenzelm@23461
   466
  fix n::nat
wenzelm@23461
   467
  {
wenzelm@23461
   468
    assume n0: "n = 0"
wenzelm@23461
   469
    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
wenzelm@23461
   470
    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
wenzelm@23461
   471
  }
wenzelm@23461
   472
  moreover
wenzelm@23461
   473
  {
wenzelm@23461
   474
    assume "\<not> n = 0"
wenzelm@23461
   475
    hence "n > 0" by simp
wenzelm@23461
   476
    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm@23461
   477
wenzelm@23461
   478
    from newInt_ex have
wenzelm@23461
   479
      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
wenzelm@23461
   480
       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
wenzelm@23461
   481
    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
wenzelm@23461
   482
    with ndef have "f n \<notin> newInt n f" by simp
wenzelm@23461
   483
  }
wenzelm@23461
   484
  ultimately have "f n \<notin> newInt n f" by (rule case_split)
wenzelm@23461
   485
  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
wenzelm@23461
   486
qed
wenzelm@23461
   487
wenzelm@23461
   488
wenzelm@23461
   489
lemma newInt_notempty:
wenzelm@23461
   490
  "(\<Inter>n. newInt n f) \<noteq> {}"
wenzelm@23461
   491
proof -
wenzelm@23461
   492
  let ?g = "\<lambda>n. newInt n f"
wenzelm@23461
   493
  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
wenzelm@23461
   494
  proof
wenzelm@23461
   495
    fix n
wenzelm@23461
   496
    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
wenzelm@23461
   497
  qed
wenzelm@23461
   498
  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
wenzelm@23461
   499
  proof
wenzelm@23461
   500
    fix n::nat
wenzelm@23461
   501
    {
wenzelm@23461
   502
      assume "n = 0"
wenzelm@23461
   503
      then have
wenzelm@23461
   504
        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
wenzelm@23461
   505
        by simp
wenzelm@23461
   506
      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
wenzelm@23461
   507
    }
wenzelm@23461
   508
    moreover
wenzelm@23461
   509
    {
wenzelm@23461
   510
      assume "\<not> n = 0"
wenzelm@23461
   511
      then have "n > 0" by simp
wenzelm@23461
   512
      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm@23461
   513
wenzelm@23461
   514
      have
wenzelm@23461
   515
        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
wenzelm@23461
   516
        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
wenzelm@23461
   517
        by (rule newInt_ex)
wenzelm@23461
   518
      then obtain a and b where
wenzelm@23461
   519
        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
wenzelm@23461
   520
      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
wenzelm@23461
   521
      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
wenzelm@23461
   522
    }
wenzelm@23461
   523
    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
wenzelm@23461
   524
  qed
wenzelm@23461
   525
  ultimately show ?thesis by (rule NIP)
wenzelm@23461
   526
qed
wenzelm@23461
   527
wenzelm@23461
   528
wenzelm@23461
   529
subsection {* Final Theorem *}
wenzelm@23461
   530
wenzelm@23461
   531
theorem real_non_denum:
wenzelm@23461
   532
  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
wenzelm@23461
   533
proof -- "by contradiction"
wenzelm@23461
   534
  assume "\<exists>f::nat\<Rightarrow>real. surj f"
hoelzl@40702
   535
  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
wenzelm@23461
   536
  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
wenzelm@23461
   537
  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
wenzelm@23461
   538
  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
wenzelm@23461
   539
  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
wenzelm@23461
   540
  moreover from rangeF have "x \<in> range f" by simp
wenzelm@23461
   541
  ultimately show False by blast
wenzelm@23461
   542
qed
wenzelm@23461
   543
wenzelm@23461
   544
end