src/HOL/Library/ContNotDenum.thy
author haftmann
Mon Mar 23 08:14:24 2009 +0100 (2009-03-23)
changeset 30663 0b6aff7451b2
parent 29026 5fbaa05f637f
child 37765 26bdfb7b680b
permissions -rw-r--r--
Main is (Complex_Main) base entry point in library theories
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
wenzelm@23461
   134
  ultimately have "\<exists>x. x\<in>A"
wenzelm@23461
   135
  proof -
wenzelm@23461
   136
    have "(0::nat) \<in> \<nat>" by simp
wenzelm@23461
   137
    moreover have "?g 0 = ?g 0" by simp
wenzelm@23461
   138
    ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
wenzelm@23461
   139
    with Adef have "?g 0 \<in> A" by simp
wenzelm@23461
   140
    thus ?thesis ..
wenzelm@23461
   141
  qed
wenzelm@23461
   142
wenzelm@23461
   143
  -- "Now show that A is bounded above ..."
wenzelm@23461
   144
  moreover have "\<exists>y. isUb (UNIV::real set) A y"
wenzelm@23461
   145
  proof -
wenzelm@23461
   146
    {
wenzelm@23461
   147
      fix n
wenzelm@23461
   148
      from ne have ex: "\<exists>x. x\<in>(f n)" ..
wenzelm@23461
   149
      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
wenzelm@23461
   150
      moreover
wenzelm@23461
   151
      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
wenzelm@23461
   152
      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
wenzelm@23461
   153
      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
wenzelm@23461
   154
      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
wenzelm@23461
   155
      with ex have "(?g n) \<le> b" by auto
wenzelm@23461
   156
      hence "\<exists>b. (?g n) \<le> b" by auto
wenzelm@23461
   157
    }
wenzelm@23461
   158
    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
wenzelm@23461
   159
wenzelm@23461
   160
    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
wenzelm@23461
   161
    proof (rule allI, induct_tac n)
wenzelm@23461
   162
      show "f 0 \<subseteq> f 0" by simp
wenzelm@23461
   163
    next
wenzelm@23461
   164
      fix n
wenzelm@23461
   165
      assume "f n \<subseteq> f 0"
wenzelm@23461
   166
      moreover from subset have "f (Suc n) \<subseteq> f n" ..
wenzelm@23461
   167
      ultimately show "f (Suc n) \<subseteq> f 0" by simp
wenzelm@23461
   168
    qed
wenzelm@23461
   169
    have "\<forall>n. (?g n)\<in>(f 0)"
wenzelm@23461
   170
    proof
wenzelm@23461
   171
      fix n
wenzelm@23461
   172
      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
wenzelm@23461
   173
      hence "?g n \<in> f n" ..
wenzelm@23461
   174
      with fs show "?g n \<in> f 0" by auto
wenzelm@23461
   175
    qed
wenzelm@23461
   176
    moreover from closed
wenzelm@23461
   177
      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
wenzelm@23461
   178
    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
wenzelm@23461
   179
    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
wenzelm@23461
   180
    with Adef have "\<forall>y\<in>A. y\<le>b" by auto
wenzelm@23461
   181
    hence "A *<= b" by (unfold setle_def)
wenzelm@23461
   182
    moreover have "b \<in> (UNIV::real set)" by simp
wenzelm@23461
   183
    ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
wenzelm@23461
   184
    hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
wenzelm@23461
   185
    thus ?thesis by auto
wenzelm@23461
   186
  qed
wenzelm@23461
   187
  -- "by the Axiom Of Completeness, A has a least upper bound ..."
wenzelm@23461
   188
  ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
wenzelm@23461
   189
wenzelm@23461
   190
  -- "denote this least upper bound as t ..."
wenzelm@23461
   191
  then obtain t where tdef: "isLub UNIV A t" ..
wenzelm@23461
   192
wenzelm@23461
   193
  -- "and finally show that this least upper bound is in all the intervals..."
wenzelm@23461
   194
  have "\<forall>n. t \<in> f n"
wenzelm@23461
   195
  proof
wenzelm@23461
   196
    fix n::nat
wenzelm@23461
   197
    from closed obtain a and b where
wenzelm@23461
   198
      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
wenzelm@23461
   199
wenzelm@23461
   200
    have "t \<ge> a"
wenzelm@23461
   201
    proof -
wenzelm@23461
   202
      have "a \<in> A"
wenzelm@23461
   203
      proof -
wenzelm@23461
   204
          (* by construction *)
wenzelm@23461
   205
        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
wenzelm@23461
   206
          using closed_int_least by blast
wenzelm@23461
   207
        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
wenzelm@23461
   208
        proof clarsimp
wenzelm@23461
   209
          fix e
wenzelm@23461
   210
          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
wenzelm@23461
   211
          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
wenzelm@23461
   212
  
wenzelm@23461
   213
          from ein aux have "a \<le> e \<and> e \<le> e" by auto
wenzelm@23461
   214
          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
wenzelm@23461
   215
          ultimately show "e = a" by simp
wenzelm@23461
   216
        qed
wenzelm@23461
   217
        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
wenzelm@23461
   218
        ultimately have "(?g n) = a" by (rule some_equality)
wenzelm@23461
   219
        moreover
wenzelm@23461
   220
        {
wenzelm@23461
   221
          have "n = of_nat n" by simp
wenzelm@23461
   222
          moreover have "of_nat n \<in> \<nat>" by simp
wenzelm@23461
   223
          ultimately have "n \<in> \<nat>"
wenzelm@23461
   224
            apply -
wenzelm@23461
   225
            apply (subst(asm) eq_sym_conv)
wenzelm@23461
   226
            apply (erule subst)
wenzelm@23461
   227
            .
wenzelm@23461
   228
        }
wenzelm@23461
   229
        with Adef have "(?g n) \<in> A" by auto
wenzelm@23461
   230
        ultimately show ?thesis by simp
wenzelm@23461
   231
      qed 
wenzelm@23461
   232
      with tdef show "a \<le> t" by (rule isLubD2)
wenzelm@23461
   233
    qed
wenzelm@23461
   234
    moreover have "t \<le> b"
wenzelm@23461
   235
    proof -
wenzelm@23461
   236
      have "isUb UNIV A b"
wenzelm@23461
   237
      proof -
wenzelm@23461
   238
        {
wenzelm@23461
   239
          from alb int have
wenzelm@23461
   240
            ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
wenzelm@23461
   241
          
wenzelm@23461
   242
          have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
wenzelm@23461
   243
          proof (rule allI, induct_tac m)
wenzelm@23461
   244
            show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
wenzelm@23461
   245
          next
wenzelm@23461
   246
            fix m n
wenzelm@23461
   247
            assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
wenzelm@23461
   248
            {
wenzelm@23461
   249
              fix p
wenzelm@23461
   250
              from pp have "f (p + n) \<subseteq> f p" by simp
wenzelm@23461
   251
              moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
wenzelm@23461
   252
              hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
wenzelm@23461
   253
              ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
wenzelm@23461
   254
            }
wenzelm@23461
   255
            thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
wenzelm@23461
   256
          qed 
wenzelm@23461
   257
          have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
wenzelm@23461
   258
          proof ((rule allI)+, rule impI)
wenzelm@23461
   259
            fix \<alpha>::nat and \<beta>::nat
wenzelm@23461
   260
            assume "\<beta> \<le> \<alpha>"
wenzelm@23461
   261
            hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
wenzelm@23461
   262
            then obtain k where "\<alpha> = \<beta> + k" ..
wenzelm@23461
   263
            moreover
wenzelm@23461
   264
            from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
wenzelm@23461
   265
            ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
wenzelm@23461
   266
          qed 
wenzelm@23461
   267
          
wenzelm@23461
   268
          fix m   
wenzelm@23461
   269
          {
wenzelm@23461
   270
            assume "m \<ge> n"
wenzelm@23461
   271
            with subsetm have "f m \<subseteq> f n" by simp
wenzelm@23461
   272
            with ain have "\<forall>x\<in>f m. x \<le> b" by auto
wenzelm@23461
   273
            moreover
wenzelm@23461
   274
            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
wenzelm@23461
   275
            ultimately have "?g m \<le> b" by auto
wenzelm@23461
   276
          }
wenzelm@23461
   277
          moreover
wenzelm@23461
   278
          {
wenzelm@23461
   279
            assume "\<not>(m \<ge> n)"
wenzelm@23461
   280
            hence "m < n" by simp
wenzelm@23461
   281
            with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
wenzelm@23461
   282
            from closed obtain ma and mb where
wenzelm@23461
   283
              "f m = closed_int ma mb \<and> ma \<le> mb" by blast
wenzelm@23461
   284
            hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
wenzelm@23461
   285
            from one alb sub fm int have "ma \<le> b" using closed_subset by blast
wenzelm@23461
   286
            moreover have "(?g m) = ma"
wenzelm@23461
   287
            proof -
wenzelm@23461
   288
              from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
wenzelm@23461
   289
              moreover from one have
wenzelm@23461
   290
                "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
wenzelm@23461
   291
                by (rule closed_int_least)
wenzelm@23461
   292
              with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
wenzelm@23461
   293
              ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
wenzelm@23461
   294
              thus "?g m = ma" by auto
wenzelm@23461
   295
            qed
wenzelm@23461
   296
            ultimately have "?g m \<le> b" by simp
wenzelm@23461
   297
          } 
wenzelm@23461
   298
          ultimately have "?g m \<le> b" by (rule case_split)
wenzelm@23461
   299
        }
wenzelm@23461
   300
        with Adef have "\<forall>y\<in>A. y\<le>b" by auto
wenzelm@23461
   301
        hence "A *<= b" by (unfold setle_def)
wenzelm@23461
   302
        moreover have "b \<in> (UNIV::real set)" by simp
wenzelm@23461
   303
        ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
wenzelm@23461
   304
        thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
wenzelm@23461
   305
      qed
wenzelm@23461
   306
      with tdef show "t \<le> b" by (rule isLub_le_isUb)
wenzelm@23461
   307
    qed
wenzelm@23461
   308
    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
wenzelm@23461
   309
    with int show "t \<in> f n" by simp
wenzelm@23461
   310
  qed
wenzelm@23461
   311
  hence "t \<in> (\<Inter>n. f n)" by auto
wenzelm@23461
   312
  thus ?thesis by auto
wenzelm@23461
   313
qed
wenzelm@23461
   314
wenzelm@23461
   315
subsection {* Generating the intervals *}
wenzelm@23461
   316
wenzelm@23461
   317
subsubsection {* Existence of non-singleton closed intervals *}
wenzelm@23461
   318
wenzelm@23461
   319
text {* This lemma asserts that given any non-singleton closed
wenzelm@23461
   320
interval (a,b) and any element c, there exists a closed interval that
wenzelm@23461
   321
is a subset of (a,b) and that does not contain c and is a
wenzelm@23461
   322
non-singleton itself. *}
wenzelm@23461
   323
wenzelm@23461
   324
lemma closed_subset_ex:
wenzelm@23461
   325
  fixes c::real
wenzelm@23461
   326
  assumes alb: "a < b"
wenzelm@23461
   327
  shows
wenzelm@23461
   328
    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
wenzelm@23461
   329
proof -
wenzelm@23461
   330
  {
wenzelm@23461
   331
    assume clb: "c < b"
wenzelm@23461
   332
    {
wenzelm@23461
   333
      assume cla: "c < a"
wenzelm@23461
   334
      from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
wenzelm@23461
   335
      with alb have
wenzelm@23461
   336
        "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
wenzelm@23461
   337
        by auto
wenzelm@23461
   338
      hence
wenzelm@23461
   339
        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
wenzelm@23461
   340
        by auto
wenzelm@23461
   341
    }
wenzelm@23461
   342
    moreover
wenzelm@23461
   343
    {
wenzelm@23461
   344
      assume ncla: "\<not>(c < a)"
wenzelm@23461
   345
      with clb have cdef: "a \<le> c \<and> c < b" by simp
wenzelm@23461
   346
      obtain ka where kadef: "ka = (c + b)/2" by blast
wenzelm@23461
   347
wenzelm@23461
   348
      from kadef clb have kalb: "ka < b" by auto
wenzelm@23461
   349
      moreover from kadef cdef have kagc: "ka > c" by simp
wenzelm@23461
   350
      ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
wenzelm@23461
   351
      moreover from cdef kagc have "ka \<ge> a" by simp
wenzelm@23461
   352
      hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
wenzelm@23461
   353
      ultimately have
wenzelm@23461
   354
        "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
wenzelm@23461
   355
        using kalb by auto
wenzelm@23461
   356
      hence
wenzelm@23461
   357
        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
wenzelm@23461
   358
        by auto
wenzelm@23461
   359
wenzelm@23461
   360
    }
wenzelm@23461
   361
    ultimately have
wenzelm@23461
   362
      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
wenzelm@23461
   363
      by (rule case_split)
wenzelm@23461
   364
  }
wenzelm@23461
   365
  moreover
wenzelm@23461
   366
  {
wenzelm@23461
   367
    assume "\<not> (c < b)"
wenzelm@23461
   368
    hence cgeb: "c \<ge> b" by simp
wenzelm@23461
   369
wenzelm@23461
   370
    obtain kb where kbdef: "kb = (a + b)/2" by blast
wenzelm@23461
   371
    with alb have kblb: "kb < b" by auto
wenzelm@23461
   372
    with kbdef cgeb have "a < kb \<and> kb < c" by auto
wenzelm@23461
   373
    moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
wenzelm@23461
   374
    moreover from kblb have
wenzelm@23461
   375
      "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
wenzelm@23461
   376
    ultimately have
wenzelm@23461
   377
      "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
wenzelm@23461
   378
      by simp
wenzelm@23461
   379
    hence
wenzelm@23461
   380
      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
wenzelm@23461
   381
      by auto
wenzelm@23461
   382
  }
wenzelm@23461
   383
  ultimately show ?thesis by (rule case_split)
wenzelm@23461
   384
qed
wenzelm@23461
   385
wenzelm@23461
   386
subsection {* newInt: Interval generation *}
wenzelm@23461
   387
wenzelm@23461
   388
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
wenzelm@23461
   389
closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
wenzelm@23461
   390
does not contain @{text "f (Suc n)"}. With the base case defined such
wenzelm@23461
   391
that @{text "(f 0)\<notin>newInt 0 f"}. *}
wenzelm@23461
   392
wenzelm@23461
   393
subsubsection {* Definition *}
wenzelm@23461
   394
haftmann@27435
   395
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
haftmann@27435
   396
  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
haftmann@27435
   397
  | "newInt (Suc n) f =
haftmann@27435
   398
      (SOME e. (\<exists>e1 e2.
haftmann@27435
   399
       e1 < e2 \<and>
haftmann@27435
   400
       e = closed_int e1 e2 \<and>
haftmann@27435
   401
       e \<subseteq> (newInt n f) \<and>
haftmann@27435
   402
       (f (Suc n)) \<notin> e)
haftmann@27435
   403
      )"
haftmann@27435
   404
haftmann@28562
   405
declare newInt.simps [code del]
wenzelm@23461
   406
wenzelm@23461
   407
subsubsection {* Properties *}
wenzelm@23461
   408
wenzelm@23461
   409
text {* We now show that every application of newInt returns an
wenzelm@23461
   410
appropriate interval. *}
wenzelm@23461
   411
wenzelm@23461
   412
lemma newInt_ex:
wenzelm@23461
   413
  "\<exists>a b. a < b \<and>
wenzelm@23461
   414
   newInt (Suc n) f = closed_int a b \<and>
wenzelm@23461
   415
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   416
   f (Suc n) \<notin> newInt (Suc n) f"
wenzelm@23461
   417
proof (induct n)
wenzelm@23461
   418
  case 0
wenzelm@23461
   419
wenzelm@23461
   420
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@23461
   421
   e1 < e2 \<and>
wenzelm@23461
   422
   e = closed_int e1 e2 \<and>
wenzelm@23461
   423
   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
wenzelm@23461
   424
   f (Suc 0) \<notin> e"
wenzelm@23461
   425
wenzelm@23461
   426
  have "newInt (Suc 0) f = ?e" by auto
wenzelm@23461
   427
  moreover
wenzelm@23461
   428
  have "f 0 + 1 < f 0 + 2" by simp
wenzelm@23461
   429
  with closed_subset_ex have
wenzelm@23461
   430
    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
wenzelm@23461
   431
     f (Suc 0) \<notin> (closed_int ka kb)" .
wenzelm@23461
   432
  hence
wenzelm@23461
   433
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
wenzelm@23461
   434
     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
wenzelm@23461
   435
  hence
wenzelm@23461
   436
    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
wenzelm@23461
   437
     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
wenzelm@23461
   438
    by (rule someI_ex)
wenzelm@23461
   439
  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
wenzelm@23461
   440
   newInt (Suc 0) f = closed_int e1 e2 \<and>
wenzelm@23461
   441
   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
wenzelm@23461
   442
   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
wenzelm@23461
   443
  thus
wenzelm@23461
   444
    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
wenzelm@23461
   445
     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
wenzelm@23461
   446
    by simp
wenzelm@23461
   447
next
wenzelm@23461
   448
  case (Suc n)
wenzelm@23461
   449
  hence "\<exists>a b.
wenzelm@23461
   450
   a < b \<and>
wenzelm@23461
   451
   newInt (Suc n) f = closed_int a b \<and>
wenzelm@23461
   452
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   453
   f (Suc n) \<notin> newInt (Suc n) f" by simp
wenzelm@23461
   454
  then obtain a and b where ab: "a < b \<and>
wenzelm@23461
   455
   newInt (Suc n) f = closed_int a b \<and>
wenzelm@23461
   456
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm@23461
   457
   f (Suc n) \<notin> newInt (Suc n) f" by auto
wenzelm@23461
   458
  hence cab: "closed_int a b = newInt (Suc n) f" by simp
wenzelm@23461
   459
wenzelm@23461
   460
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm@23461
   461
    e1 < e2 \<and>
wenzelm@23461
   462
    e = closed_int e1 e2 \<and>
wenzelm@23461
   463
    e \<subseteq> closed_int a b \<and>
wenzelm@23461
   464
    f (Suc (Suc n)) \<notin> e"
wenzelm@23461
   465
  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
wenzelm@23461
   466
wenzelm@23461
   467
  from ab have "a < b" by simp
wenzelm@23461
   468
  with closed_subset_ex have
wenzelm@23461
   469
    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
wenzelm@23461
   470
     f (Suc (Suc n)) \<notin> closed_int ka kb" .
wenzelm@23461
   471
  hence
wenzelm@23461
   472
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
wenzelm@23461
   473
     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
wenzelm@23461
   474
    by simp
wenzelm@23461
   475
  hence
wenzelm@23461
   476
    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
wenzelm@23461
   477
     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
wenzelm@23461
   478
  hence
wenzelm@23461
   479
    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
wenzelm@23461
   480
     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
wenzelm@23461
   481
  with ab ni show
wenzelm@23461
   482
    "\<exists>ka kb. ka < kb \<and>
wenzelm@23461
   483
     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
wenzelm@23461
   484
     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
wenzelm@23461
   485
     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
wenzelm@23461
   486
qed
wenzelm@23461
   487
wenzelm@23461
   488
lemma newInt_subset:
wenzelm@23461
   489
  "newInt (Suc n) f \<subseteq> newInt n f"
wenzelm@23461
   490
  using newInt_ex by auto
wenzelm@23461
   491
wenzelm@23461
   492
wenzelm@23461
   493
text {* Another fundamental property is that no element in the range
wenzelm@23461
   494
of f is in the intersection of all closed intervals generated by
wenzelm@23461
   495
newInt. *}
wenzelm@23461
   496
wenzelm@23461
   497
lemma newInt_inter:
wenzelm@23461
   498
  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
wenzelm@23461
   499
proof
wenzelm@23461
   500
  fix n::nat
wenzelm@23461
   501
  {
wenzelm@23461
   502
    assume n0: "n = 0"
wenzelm@23461
   503
    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
wenzelm@23461
   504
    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
wenzelm@23461
   505
  }
wenzelm@23461
   506
  moreover
wenzelm@23461
   507
  {
wenzelm@23461
   508
    assume "\<not> n = 0"
wenzelm@23461
   509
    hence "n > 0" by simp
wenzelm@23461
   510
    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm@23461
   511
wenzelm@23461
   512
    from newInt_ex have
wenzelm@23461
   513
      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
wenzelm@23461
   514
       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
wenzelm@23461
   515
    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
wenzelm@23461
   516
    with ndef have "f n \<notin> newInt n f" by simp
wenzelm@23461
   517
  }
wenzelm@23461
   518
  ultimately have "f n \<notin> newInt n f" by (rule case_split)
wenzelm@23461
   519
  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
wenzelm@23461
   520
qed
wenzelm@23461
   521
wenzelm@23461
   522
wenzelm@23461
   523
lemma newInt_notempty:
wenzelm@23461
   524
  "(\<Inter>n. newInt n f) \<noteq> {}"
wenzelm@23461
   525
proof -
wenzelm@23461
   526
  let ?g = "\<lambda>n. newInt n f"
wenzelm@23461
   527
  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
wenzelm@23461
   528
  proof
wenzelm@23461
   529
    fix n
wenzelm@23461
   530
    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
wenzelm@23461
   531
  qed
wenzelm@23461
   532
  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
wenzelm@23461
   533
  proof
wenzelm@23461
   534
    fix n::nat
wenzelm@23461
   535
    {
wenzelm@23461
   536
      assume "n = 0"
wenzelm@23461
   537
      then have
wenzelm@23461
   538
        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
wenzelm@23461
   539
        by simp
wenzelm@23461
   540
      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
wenzelm@23461
   541
    }
wenzelm@23461
   542
    moreover
wenzelm@23461
   543
    {
wenzelm@23461
   544
      assume "\<not> n = 0"
wenzelm@23461
   545
      then have "n > 0" by simp
wenzelm@23461
   546
      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm@23461
   547
wenzelm@23461
   548
      have
wenzelm@23461
   549
        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
wenzelm@23461
   550
        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
wenzelm@23461
   551
        by (rule newInt_ex)
wenzelm@23461
   552
      then obtain a and b where
wenzelm@23461
   553
        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
wenzelm@23461
   554
      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
wenzelm@23461
   555
      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
wenzelm@23461
   556
    }
wenzelm@23461
   557
    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
wenzelm@23461
   558
  qed
wenzelm@23461
   559
  ultimately show ?thesis by (rule NIP)
wenzelm@23461
   560
qed
wenzelm@23461
   561
wenzelm@23461
   562
wenzelm@23461
   563
subsection {* Final Theorem *}
wenzelm@23461
   564
wenzelm@23461
   565
theorem real_non_denum:
wenzelm@23461
   566
  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
wenzelm@23461
   567
proof -- "by contradiction"
wenzelm@23461
   568
  assume "\<exists>f::nat\<Rightarrow>real. surj f"
wenzelm@23461
   569
  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
wenzelm@23461
   570
  hence rangeF: "range f = UNIV" by (rule surj_range)
wenzelm@23461
   571
  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
wenzelm@23461
   572
  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
wenzelm@23461
   573
  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
wenzelm@23461
   574
  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
wenzelm@23461
   575
  moreover from rangeF have "x \<in> range f" by simp
wenzelm@23461
   576
  ultimately show False by blast
wenzelm@23461
   577
qed
wenzelm@23461
   578
wenzelm@23461
   579
end