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