src/HOL/Library/ContNotDenum.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 40702 cf26dd7395e4
child 53372 f5a6313c7fe4
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     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 Complex_Main
     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 
   406 subsubsection {* Properties *}
   407 
   408 text {* We now show that every application of newInt returns an
   409 appropriate interval. *}
   410 
   411 lemma newInt_ex:
   412   "\<exists>a b. a < b \<and>
   413    newInt (Suc n) f = closed_int a b \<and>
   414    newInt (Suc n) f \<subseteq> newInt n f \<and>
   415    f (Suc n) \<notin> newInt (Suc n) f"
   416 proof (induct n)
   417   case 0
   418 
   419   let ?e = "SOME e. \<exists>e1 e2.
   420    e1 < e2 \<and>
   421    e = closed_int e1 e2 \<and>
   422    e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   423    f (Suc 0) \<notin> e"
   424 
   425   have "newInt (Suc 0) f = ?e" by auto
   426   moreover
   427   have "f 0 + 1 < f 0 + 2" by simp
   428   with closed_subset_ex have
   429     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   430      f (Suc 0) \<notin> (closed_int ka kb)" .
   431   hence
   432     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   433      e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
   434   hence
   435     "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   436      ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
   437     by (rule someI_ex)
   438   ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   439    newInt (Suc 0) f = closed_int e1 e2 \<and>
   440    newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   441    f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   442   thus
   443     "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
   444      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   445     by simp
   446 next
   447   case (Suc n)
   448   hence "\<exists>a b.
   449    a < b \<and>
   450    newInt (Suc n) f = closed_int a b \<and>
   451    newInt (Suc n) f \<subseteq> newInt n f \<and>
   452    f (Suc n) \<notin> newInt (Suc n) f" by simp
   453   then obtain a and b where ab: "a < b \<and>
   454    newInt (Suc n) f = closed_int a b \<and>
   455    newInt (Suc n) f \<subseteq> newInt n f \<and>
   456    f (Suc n) \<notin> newInt (Suc n) f" by auto
   457   hence cab: "closed_int a b = newInt (Suc n) f" by simp
   458 
   459   let ?e = "SOME e. \<exists>e1 e2.
   460     e1 < e2 \<and>
   461     e = closed_int e1 e2 \<and>
   462     e \<subseteq> closed_int a b \<and>
   463     f (Suc (Suc n)) \<notin> e"
   464   from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   465 
   466   from ab have "a < b" by simp
   467   with closed_subset_ex have
   468     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
   469      f (Suc (Suc n)) \<notin> closed_int ka kb" .
   470   hence
   471     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   472      closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
   473     by simp
   474   hence
   475     "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   476      e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
   477   hence
   478     "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   479      ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   480   with ab ni show
   481     "\<exists>ka kb. ka < kb \<and>
   482      newInt (Suc (Suc n)) f = closed_int ka kb \<and>
   483      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   484      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   485 qed
   486 
   487 lemma newInt_subset:
   488   "newInt (Suc n) f \<subseteq> newInt n f"
   489   using newInt_ex by auto
   490 
   491 
   492 text {* Another fundamental property is that no element in the range
   493 of f is in the intersection of all closed intervals generated by
   494 newInt. *}
   495 
   496 lemma newInt_inter:
   497   "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   498 proof
   499   fix n::nat
   500   {
   501     assume n0: "n = 0"
   502     moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
   503     ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
   504   }
   505   moreover
   506   {
   507     assume "\<not> n = 0"
   508     hence "n > 0" by simp
   509     then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   510 
   511     from newInt_ex have
   512       "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   513        newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   514     then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   515     with ndef have "f n \<notin> newInt n f" by simp
   516   }
   517   ultimately have "f n \<notin> newInt n f" by (rule case_split)
   518   thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   519 qed
   520 
   521 
   522 lemma newInt_notempty:
   523   "(\<Inter>n. newInt n f) \<noteq> {}"
   524 proof -
   525   let ?g = "\<lambda>n. newInt n f"
   526   have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   527   proof
   528     fix n
   529     show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   530   qed
   531   moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
   532   proof
   533     fix n::nat
   534     {
   535       assume "n = 0"
   536       then have
   537         "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
   538         by simp
   539       hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   540     }
   541     moreover
   542     {
   543       assume "\<not> n = 0"
   544       then have "n > 0" by simp
   545       then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   546 
   547       have
   548         "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   549         (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   550         by (rule newInt_ex)
   551       then obtain a and b where
   552         "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
   553       with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
   554       hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   555     }
   556     ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
   557   qed
   558   ultimately show ?thesis by (rule NIP)
   559 qed
   560 
   561 
   562 subsection {* Final Theorem *}
   563 
   564 theorem real_non_denum:
   565   shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   566 proof -- "by contradiction"
   567   assume "\<exists>f::nat\<Rightarrow>real. surj f"
   568   then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
   569   -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   570   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   571   moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   572   ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   573   moreover from rangeF have "x \<in> range f" by simp
   574   ultimately show False by blast
   575 qed
   576 
   577 end