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