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