src/HOL/Library/ContNotDenum.thy
author nipkow
Wed Dec 10 10:23:47 2008 +0100 (2008-12-10)
changeset 29026 5fbaa05f637f
parent 28952 src/HOL/ContNotDenum.thy@15a4b2cf8c34
child 30663 0b6aff7451b2
permissions -rw-r--r--
moved ContNotDenum into Library
     1 (*  Title       : HOL/ContNonDenum
     2     Author      : Benjamin Porter, Monash University, NICTA, 2005
     3 *)
     4 
     5 header {* Non-denumerability of the Continuum. *}
     6 
     7 theory ContNotDenum
     8 imports RComplete Hilbert_Choice
     9 begin
    10 
    11 subsection {* Abstract *}
    12 
    13 text {* The following document presents a proof that the Continuum is
    14 uncountable. It is formalised in the Isabelle/Isar theorem proving
    15 system.
    16 
    17 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    18 words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    19 surjective.
    20 
    21 {\em Outline:} An elegant informal proof of this result uses Cantor's
    22 Diagonalisation argument. The proof presented here is not this
    23 one. First we formalise some properties of closed intervals, then we
    24 prove the Nested Interval Property. This property relies on the
    25 completeness of the Real numbers and is the foundation for our
    26 argument. Informally it states that an intersection of countable
    27 closed intervals (where each successive interval is a subset of the
    28 last) is non-empty. We then assume a surjective function f:@{text
    29 "\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
    30 by generating a sequence of closed intervals then using the NIP. *}
    31 
    32 subsection {* Closed Intervals *}
    33 
    34 text {* This section formalises some properties of closed intervals. *}
    35 
    36 subsubsection {* Definition *}
    37 
    38 definition
    39   closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
    40   "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
    41 
    42 subsubsection {* Properties *}
    43 
    44 lemma closed_int_subset:
    45   assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
    46   shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
    47 proof -
    48   {
    49     fix x::real
    50     assume "x \<in> closed_int x1 y1"
    51     hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
    52     with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
    53     hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
    54   }
    55   thus ?thesis by auto
    56 qed
    57 
    58 lemma closed_int_least:
    59   assumes a: "a \<le> b"
    60   shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
    61 proof
    62   from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    63   thus "a \<in> closed_int a b" by (unfold closed_int_def)
    64 next
    65   have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
    66   thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
    67 qed
    68 
    69 lemma closed_int_most:
    70   assumes a: "a \<le> b"
    71   shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
    72 proof
    73   from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    74   thus "b \<in> closed_int a b" by (unfold closed_int_def)
    75 next
    76   have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
    77   thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
    78 qed
    79 
    80 lemma closed_not_empty:
    81   shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 
    82   by (auto dest: closed_int_least)
    83 
    84 lemma closed_mem:
    85   assumes "a \<le> c" and "c \<le> b"
    86   shows "c \<in> closed_int a b"
    87   using assms unfolding closed_int_def by auto
    88 
    89 lemma closed_subset:
    90   assumes ac: "a \<le> b"  "c \<le> d" 
    91   assumes closed: "closed_int a b \<subseteq> closed_int c d"
    92   shows "b \<ge> c"
    93 proof -
    94   from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
    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)
    96   with ac have "c\<le>b \<and> b\<le>d" by simp
    97   thus ?thesis by auto
    98 qed
    99 
   100 
   101 subsection {* Nested Interval Property *}
   102 
   103 theorem NIP:
   104   fixes f::"nat \<Rightarrow> real set"
   105   assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
   106   and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
   107   shows "(\<Inter>n. f n) \<noteq> {}"
   108 proof -
   109   let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
   110   have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
   111   proof
   112     fix n
   113     from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
   114     then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
   115     hence "a \<le> b" ..
   116     with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
   117     with fn show "\<exists>x. x\<in>(f n)" by simp
   118   qed
   119 
   120   have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
   121   proof
   122     fix n
   123     from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   124     then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
   125     hence "a \<le> b" by simp
   126     hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
   127     with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
   128     hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
   129     thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
   130   qed
   131 
   132   -- "A denotes the set of all left-most points of all the intervals ..."
   133   moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
   134   ultimately have "\<exists>x. x\<in>A"
   135   proof -
   136     have "(0::nat) \<in> \<nat>" by simp
   137     moreover have "?g 0 = ?g 0" by simp
   138     ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
   139     with Adef have "?g 0 \<in> A" by simp
   140     thus ?thesis ..
   141   qed
   142 
   143   -- "Now show that A is bounded above ..."
   144   moreover have "\<exists>y. isUb (UNIV::real set) A y"
   145   proof -
   146     {
   147       fix n
   148       from ne have ex: "\<exists>x. x\<in>(f n)" ..
   149       from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   150       moreover
   151       from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   152       then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
   153       hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
   154       ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
   155       with ex have "(?g n) \<le> b" by auto
   156       hence "\<exists>b. (?g n) \<le> b" by auto
   157     }
   158     hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
   159 
   160     have fs: "\<forall>n::nat. f n \<subseteq> f 0"
   161     proof (rule allI, induct_tac n)
   162       show "f 0 \<subseteq> f 0" by simp
   163     next
   164       fix n
   165       assume "f n \<subseteq> f 0"
   166       moreover from subset have "f (Suc n) \<subseteq> f n" ..
   167       ultimately show "f (Suc n) \<subseteq> f 0" by simp
   168     qed
   169     have "\<forall>n. (?g n)\<in>(f 0)"
   170     proof
   171       fix n
   172       from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   173       hence "?g n \<in> f n" ..
   174       with fs show "?g n \<in> f 0" by auto
   175     qed
   176     moreover from closed
   177       obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
   178     ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
   179     with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
   180     with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   181     hence "A *<= b" by (unfold setle_def)
   182     moreover have "b \<in> (UNIV::real set)" by simp
   183     ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   184     hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
   185     thus ?thesis by auto
   186   qed
   187   -- "by the Axiom Of Completeness, A has a least upper bound ..."
   188   ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
   189 
   190   -- "denote this least upper bound as t ..."
   191   then obtain t where tdef: "isLub UNIV A t" ..
   192 
   193   -- "and finally show that this least upper bound is in all the intervals..."
   194   have "\<forall>n. t \<in> f n"
   195   proof
   196     fix n::nat
   197     from closed obtain a and b where
   198       int: "f n = closed_int a b" and alb: "a \<le> b" by blast
   199 
   200     have "t \<ge> a"
   201     proof -
   202       have "a \<in> A"
   203       proof -
   204           (* by construction *)
   205         from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
   206           using closed_int_least by blast
   207         moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
   208         proof clarsimp
   209           fix e
   210           assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
   211           from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
   212   
   213           from ein aux have "a \<le> e \<and> e \<le> e" by auto
   214           moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
   215           ultimately show "e = a" by simp
   216         qed
   217         hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
   218         ultimately have "(?g n) = a" by (rule some_equality)
   219         moreover
   220         {
   221           have "n = of_nat n" by simp
   222           moreover have "of_nat n \<in> \<nat>" by simp
   223           ultimately have "n \<in> \<nat>"
   224             apply -
   225             apply (subst(asm) eq_sym_conv)
   226             apply (erule subst)
   227             .
   228         }
   229         with Adef have "(?g n) \<in> A" by auto
   230         ultimately show ?thesis by simp
   231       qed 
   232       with tdef show "a \<le> t" by (rule isLubD2)
   233     qed
   234     moreover have "t \<le> b"
   235     proof -
   236       have "isUb UNIV A b"
   237       proof -
   238         {
   239           from alb int have
   240             ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
   241           
   242           have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
   243           proof (rule allI, induct_tac m)
   244             show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
   245           next
   246             fix m n
   247             assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
   248             {
   249               fix p
   250               from pp have "f (p + n) \<subseteq> f p" by simp
   251               moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
   252               hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
   253               ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
   254             }
   255             thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
   256           qed 
   257           have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
   258           proof ((rule allI)+, rule impI)
   259             fix \<alpha>::nat and \<beta>::nat
   260             assume "\<beta> \<le> \<alpha>"
   261             hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
   262             then obtain k where "\<alpha> = \<beta> + k" ..
   263             moreover
   264             from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
   265             ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
   266           qed 
   267           
   268           fix m   
   269           {
   270             assume "m \<ge> n"
   271             with subsetm have "f m \<subseteq> f n" by simp
   272             with ain have "\<forall>x\<in>f m. x \<le> b" by auto
   273             moreover
   274             from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
   275             ultimately have "?g m \<le> b" by auto
   276           }
   277           moreover
   278           {
   279             assume "\<not>(m \<ge> n)"
   280             hence "m < n" by simp
   281             with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
   282             from closed obtain ma and mb where
   283               "f m = closed_int ma mb \<and> ma \<le> mb" by blast
   284             hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
   285             from one alb sub fm int have "ma \<le> b" using closed_subset by blast
   286             moreover have "(?g m) = ma"
   287             proof -
   288               from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
   289               moreover from one have
   290                 "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
   291                 by (rule closed_int_least)
   292               with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
   293               ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
   294               thus "?g m = ma" by auto
   295             qed
   296             ultimately have "?g m \<le> b" by simp
   297           } 
   298           ultimately have "?g m \<le> b" by (rule case_split)
   299         }
   300         with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   301         hence "A *<= b" by (unfold setle_def)
   302         moreover have "b \<in> (UNIV::real set)" by simp
   303         ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   304         thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
   305       qed
   306       with tdef show "t \<le> b" by (rule isLub_le_isUb)
   307     qed
   308     ultimately have "t \<in> closed_int a b" by (rule closed_mem)
   309     with int show "t \<in> f n" by simp
   310   qed
   311   hence "t \<in> (\<Inter>n. f n)" by auto
   312   thus ?thesis by auto
   313 qed
   314 
   315 subsection {* Generating the intervals *}
   316 
   317 subsubsection {* Existence of non-singleton closed intervals *}
   318 
   319 text {* This lemma asserts that given any non-singleton closed
   320 interval (a,b) and any element c, there exists a closed interval that
   321 is a subset of (a,b) and that does not contain c and is a
   322 non-singleton itself. *}
   323 
   324 lemma closed_subset_ex:
   325   fixes c::real
   326   assumes alb: "a < b"
   327   shows
   328     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   329 proof -
   330   {
   331     assume clb: "c < b"
   332     {
   333       assume cla: "c < a"
   334       from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
   335       with alb have
   336         "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
   337         by auto
   338       hence
   339         "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   340         by auto
   341     }
   342     moreover
   343     {
   344       assume ncla: "\<not>(c < a)"
   345       with clb have cdef: "a \<le> c \<and> c < b" by simp
   346       obtain ka where kadef: "ka = (c + b)/2" by blast
   347 
   348       from kadef clb have kalb: "ka < b" by auto
   349       moreover from kadef cdef have kagc: "ka > c" by simp
   350       ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
   351       moreover from cdef kagc have "ka \<ge> a" by simp
   352       hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   353       ultimately have
   354         "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
   355         using kalb by auto
   356       hence
   357         "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   358         by auto
   359 
   360     }
   361     ultimately have
   362       "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   363       by (rule case_split)
   364   }
   365   moreover
   366   {
   367     assume "\<not> (c < b)"
   368     hence cgeb: "c \<ge> b" by simp
   369 
   370     obtain kb where kbdef: "kb = (a + b)/2" by blast
   371     with alb have kblb: "kb < b" by auto
   372     with kbdef cgeb have "a < kb \<and> kb < c" by auto
   373     moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
   374     moreover from kblb have
   375       "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   376     ultimately have
   377       "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
   378       by simp
   379     hence
   380       "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
   381       by auto
   382   }
   383   ultimately show ?thesis by (rule case_split)
   384 qed
   385 
   386 subsection {* newInt: Interval generation *}
   387 
   388 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   389 closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
   390 does not contain @{text "f (Suc n)"}. With the base case defined such
   391 that @{text "(f 0)\<notin>newInt 0 f"}. *}
   392 
   393 subsubsection {* Definition *}
   394 
   395 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   396   "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
   397   | "newInt (Suc n) f =
   398       (SOME e. (\<exists>e1 e2.
   399        e1 < e2 \<and>
   400        e = closed_int e1 e2 \<and>
   401        e \<subseteq> (newInt n f) \<and>
   402        (f (Suc n)) \<notin> e)
   403       )"
   404 
   405 declare newInt.simps [code del]
   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