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
`