src/HOL/Real/ContNotDenum.thy
 author nipkow Tue Oct 23 23:27:23 2007 +0200 (2007-10-23) changeset 25162 ad4d5365d9d8 parent 23461 9a586e80ce15 child 27368 9f90ac19e32b permissions -rw-r--r--
went back to >0
     1 (*  Title       : HOL/Real/ContNonDenum

     2     ID          : $Id$

     3     Author      : Benjamin Porter, Monash University, NICTA, 2005

     4 *)

     5

     6 header {* Non-denumerability of the Continuum. *}

     7

     8 theory ContNotDenum

     9 imports RComplete

    10 begin

    11

    12 subsection {* Abstract *}

    13

    14 text {* The following document presents a proof that the Continuum is

    15 uncountable. It is formalised in the Isabelle/Isar theorem proving

    16 system.

    17

    18 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other

    19 words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is

    20 surjective.

    21

    22 {\em Outline:} An elegant informal proof of this result uses Cantor's

    23 Diagonalisation argument. The proof presented here is not this

    24 one. First we formalise some properties of closed intervals, then we

    25 prove the Nested Interval Property. This property relies on the

    26 completeness of the Real numbers and is the foundation for our

    27 argument. Informally it states that an intersection of countable

    28 closed intervals (where each successive interval is a subset of the

    29 last) is non-empty. We then assume a surjective function f:@{text

    30 "\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f

    31 by generating a sequence of closed intervals then using the NIP. *}

    32

    33 subsection {* Closed Intervals *}

    34

    35 text {* This section formalises some properties of closed intervals. *}

    36

    37 subsubsection {* Definition *}

    38

    39 definition

    40   closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where

    41   "closed_int x y = {z. x \<le> z \<and> z \<le> y}"

    42

    43 subsubsection {* Properties *}

    44

    45 lemma closed_int_subset:

    46   assumes xy: "x1 \<ge> x0" "y1 \<le> y0"

    47   shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"

    48 proof -

    49   {

    50     fix x::real

    51     assume "x \<in> closed_int x1 y1"

    52     hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)

    53     with xy have "x \<ge> x0 \<and> x \<le> y0" by auto

    54     hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)

    55   }

    56   thus ?thesis by auto

    57 qed

    58

    59 lemma closed_int_least:

    60   assumes a: "a \<le> b"

    61   shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"

    62 proof

    63   from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp

    64   thus "a \<in> closed_int a b" by (unfold closed_int_def)

    65 next

    66   have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp

    67   thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)

    68 qed

    69

    70 lemma closed_int_most:

    71   assumes a: "a \<le> b"

    72   shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"

    73 proof

    74   from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp

    75   thus "b \<in> closed_int a b" by (unfold closed_int_def)

    76 next

    77   have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp

    78   thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)

    79 qed

    80

    81 lemma closed_not_empty:

    82   shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b"

    83   by (auto dest: closed_int_least)

    84

    85 lemma closed_mem:

    86   assumes "a \<le> c" and "c \<le> b"

    87   shows "c \<in> closed_int a b"

    88   using assms unfolding closed_int_def by auto

    89

    90 lemma closed_subset:

    91   assumes ac: "a \<le> b"  "c \<le> d"

    92   assumes closed: "closed_int a b \<subseteq> closed_int c d"

    93   shows "b \<ge> c"

    94 proof -

    95   from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto

    96   hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)

    97   with ac have "c\<le>b \<and> b\<le>d" by simp

    98   thus ?thesis by auto

    99 qed

   100

   101

   102 subsection {* Nested Interval Property *}

   103

   104 theorem NIP:

   105   fixes f::"nat \<Rightarrow> real set"

   106   assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"

   107   and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"

   108   shows "(\<Inter>n. f n) \<noteq> {}"

   109 proof -

   110   let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"

   111   have ne: "\<forall>n. \<exists>x. x\<in>(f n)"

   112   proof

   113     fix n

   114     from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp

   115     then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto

   116     hence "a \<le> b" ..

   117     with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp

   118     with fn show "\<exists>x. x\<in>(f n)" by simp

   119   qed

   120

   121   have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"

   122   proof

   123     fix n

   124     from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..

   125     then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto

   126     hence "a \<le> b" by simp

   127     hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)

   128     with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp

   129     hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..

   130     thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)

   131   qed

   132

   133   -- "A denotes the set of all left-most points of all the intervals ..."

   134   moreover obtain A where Adef: "A = ?g  \<nat>" by simp

   135   ultimately have "\<exists>x. x\<in>A"

   136   proof -

   137     have "(0::nat) \<in> \<nat>" by simp

   138     moreover have "?g 0 = ?g 0" by simp

   139     ultimately have "?g 0 \<in> ?g  \<nat>" by (rule  rev_image_eqI)

   140     with Adef have "?g 0 \<in> A" by simp

   141     thus ?thesis ..

   142   qed

   143

   144   -- "Now show that A is bounded above ..."

   145   moreover have "\<exists>y. isUb (UNIV::real set) A y"

   146   proof -

   147     {

   148       fix n

   149       from ne have ex: "\<exists>x. x\<in>(f n)" ..

   150       from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp

   151       moreover

   152       from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..

   153       then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto

   154       hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast

   155       ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp

   156       with ex have "(?g n) \<le> b" by auto

   157       hence "\<exists>b. (?g n) \<le> b" by auto

   158     }

   159     hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..

   160

   161     have fs: "\<forall>n::nat. f n \<subseteq> f 0"

   162     proof (rule allI, induct_tac n)

   163       show "f 0 \<subseteq> f 0" by simp

   164     next

   165       fix n

   166       assume "f n \<subseteq> f 0"

   167       moreover from subset have "f (Suc n) \<subseteq> f n" ..

   168       ultimately show "f (Suc n) \<subseteq> f 0" by simp

   169     qed

   170     have "\<forall>n. (?g n)\<in>(f 0)"

   171     proof

   172       fix n

   173       from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp

   174       hence "?g n \<in> f n" ..

   175       with fs show "?g n \<in> f 0" by auto

   176     qed

   177     moreover from closed

   178       obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast

   179     ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto

   180     with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast

   181     with Adef have "\<forall>y\<in>A. y\<le>b" by auto

   182     hence "A *<= b" by (unfold setle_def)

   183     moreover have "b \<in> (UNIV::real set)" by simp

   184     ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp

   185     hence "isUb (UNIV::real set) A b" by (unfold isUb_def)

   186     thus ?thesis by auto

   187   qed

   188   -- "by the Axiom Of Completeness, A has a least upper bound ..."

   189   ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)

   190

   191   -- "denote this least upper bound as t ..."

   192   then obtain t where tdef: "isLub UNIV A t" ..

   193

   194   -- "and finally show that this least upper bound is in all the intervals..."

   195   have "\<forall>n. t \<in> f n"

   196   proof

   197     fix n::nat

   198     from closed obtain a and b where

   199       int: "f n = closed_int a b" and alb: "a \<le> b" by blast

   200

   201     have "t \<ge> a"

   202     proof -

   203       have "a \<in> A"

   204       proof -

   205           (* by construction *)

   206         from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"

   207           using closed_int_least by blast

   208         moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"

   209         proof clarsimp

   210           fix e

   211           assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"

   212           from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto

   213

   214           from ein aux have "a \<le> e \<and> e \<le> e" by auto

   215           moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto

   216           ultimately show "e = a" by simp

   217         qed

   218         hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp

   219         ultimately have "(?g n) = a" by (rule some_equality)

   220         moreover

   221         {

   222           have "n = of_nat n" by simp

   223           moreover have "of_nat n \<in> \<nat>" by simp

   224           ultimately have "n \<in> \<nat>"

   225             apply -

   226             apply (subst(asm) eq_sym_conv)

   227             apply (erule subst)

   228             .

   229         }

   230         with Adef have "(?g n) \<in> A" by auto

   231         ultimately show ?thesis by simp

   232       qed

   233       with tdef show "a \<le> t" by (rule isLubD2)

   234     qed

   235     moreover have "t \<le> b"

   236     proof -

   237       have "isUb UNIV A b"

   238       proof -

   239         {

   240           from alb int have

   241             ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast

   242

   243           have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"

   244           proof (rule allI, induct_tac m)

   245             show "\<forall>n. f (n + 0) \<subseteq> f n" by simp

   246           next

   247             fix m n

   248             assume pp: "\<forall>p. f (p + n) \<subseteq> f p"

   249             {

   250               fix p

   251               from pp have "f (p + n) \<subseteq> f p" by simp

   252               moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto

   253               hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp

   254               ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp

   255             }

   256             thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..

   257           qed

   258           have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"

   259           proof ((rule allI)+, rule impI)

   260             fix \<alpha>::nat and \<beta>::nat

   261             assume "\<beta> \<le> \<alpha>"

   262             hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)

   263             then obtain k where "\<alpha> = \<beta> + k" ..

   264             moreover

   265             from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp

   266             ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto

   267           qed

   268

   269           fix m

   270           {

   271             assume "m \<ge> n"

   272             with subsetm have "f m \<subseteq> f n" by simp

   273             with ain have "\<forall>x\<in>f m. x \<le> b" by auto

   274             moreover

   275             from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp

   276             ultimately have "?g m \<le> b" by auto

   277           }

   278           moreover

   279           {

   280             assume "\<not>(m \<ge> n)"

   281             hence "m < n" by simp

   282             with subsetm have sub: "(f n) \<subseteq> (f m)" by simp

   283             from closed obtain ma and mb where

   284               "f m = closed_int ma mb \<and> ma \<le> mb" by blast

   285             hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto

   286             from one alb sub fm int have "ma \<le> b" using closed_subset by blast

   287             moreover have "(?g m) = ma"

   288             proof -

   289               from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..

   290               moreover from one have

   291                 "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"

   292                 by (rule closed_int_least)

   293               with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp

   294               ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto

   295               thus "?g m = ma" by auto

   296             qed

   297             ultimately have "?g m \<le> b" by simp

   298           }

   299           ultimately have "?g m \<le> b" by (rule case_split)

   300         }

   301         with Adef have "\<forall>y\<in>A. y\<le>b" by auto

   302         hence "A *<= b" by (unfold setle_def)

   303         moreover have "b \<in> (UNIV::real set)" by simp

   304         ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp

   305         thus "isUb (UNIV::real set) A b" by (unfold isUb_def)

   306       qed

   307       with tdef show "t \<le> b" by (rule isLub_le_isUb)

   308     qed

   309     ultimately have "t \<in> closed_int a b" by (rule closed_mem)

   310     with int show "t \<in> f n" by simp

   311   qed

   312   hence "t \<in> (\<Inter>n. f n)" by auto

   313   thus ?thesis by auto

   314 qed

   315

   316 subsection {* Generating the intervals *}

   317

   318 subsubsection {* Existence of non-singleton closed intervals *}

   319

   320 text {* This lemma asserts that given any non-singleton closed

   321 interval (a,b) and any element c, there exists a closed interval that

   322 is a subset of (a,b) and that does not contain c and is a

   323 non-singleton itself. *}

   324

   325 lemma closed_subset_ex:

   326   fixes c::real

   327   assumes alb: "a < b"

   328   shows

   329     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"

   330 proof -

   331   {

   332     assume clb: "c < b"

   333     {

   334       assume cla: "c < a"

   335       from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)

   336       with alb have

   337         "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"

   338         by auto

   339       hence

   340         "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"

   341         by auto

   342     }

   343     moreover

   344     {

   345       assume ncla: "\<not>(c < a)"

   346       with clb have cdef: "a \<le> c \<and> c < b" by simp

   347       obtain ka where kadef: "ka = (c + b)/2" by blast

   348

   349       from kadef clb have kalb: "ka < b" by auto

   350       moreover from kadef cdef have kagc: "ka > c" by simp

   351       ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)

   352       moreover from cdef kagc have "ka \<ge> a" by simp

   353       hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)

   354       ultimately have

   355         "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"

   356         using kalb by auto

   357       hence

   358         "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"

   359         by auto

   360

   361     }

   362     ultimately have

   363       "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"

   364       by (rule case_split)

   365   }

   366   moreover

   367   {

   368     assume "\<not> (c < b)"

   369     hence cgeb: "c \<ge> b" by simp

   370

   371     obtain kb where kbdef: "kb = (a + b)/2" by blast

   372     with alb have kblb: "kb < b" by auto

   373     with kbdef cgeb have "a < kb \<and> kb < c" by auto

   374     moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)

   375     moreover from kblb have

   376       "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)

   377     ultimately have

   378       "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"

   379       by simp

   380     hence

   381       "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"

   382       by auto

   383   }

   384   ultimately show ?thesis by (rule case_split)

   385 qed

   386

   387 subsection {* newInt: Interval generation *}

   388

   389 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a

   390 closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and

   391 does not contain @{text "f (Suc n)"}. With the base case defined such

   392 that @{text "(f 0)\<notin>newInt 0 f"}. *}

   393

   394 subsubsection {* Definition *}

   395

   396 consts newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"

   397 primrec

   398 "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"

   399 "newInt (Suc n) f =

   400   (SOME e. (\<exists>e1 e2.

   401    e1 < e2 \<and>

   402    e = closed_int e1 e2 \<and>

   403    e \<subseteq> (newInt n f) \<and>

   404    (f (Suc n)) \<notin> e)

   405   )"

   406

   407 subsubsection {* Properties *}

   408

   409 text {* We now show that every application of newInt returns an

   410 appropriate interval. *}

   411

   412 lemma newInt_ex:

   413   "\<exists>a b. a < b \<and>

   414    newInt (Suc n) f = closed_int a b \<and>

   415    newInt (Suc n) f \<subseteq> newInt n f \<and>

   416    f (Suc n) \<notin> newInt (Suc n) f"

   417 proof (induct n)

   418   case 0

   419

   420   let ?e = "SOME e. \<exists>e1 e2.

   421    e1 < e2 \<and>

   422    e = closed_int e1 e2 \<and>

   423    e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

   424    f (Suc 0) \<notin> e"

   425

   426   have "newInt (Suc 0) f = ?e" by auto

   427   moreover

   428   have "f 0 + 1 < f 0 + 2" by simp

   429   with closed_subset_ex have

   430     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

   431      f (Suc 0) \<notin> (closed_int ka kb)" .

   432   hence

   433     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

   434      e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp

   435   hence

   436     "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>

   437      ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"

   438     by (rule someI_ex)

   439   ultimately have "\<exists>e1 e2. e1 < e2 \<and>

   440    newInt (Suc 0) f = closed_int e1 e2 \<and>

   441    newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

   442    f (Suc 0) \<notin> newInt (Suc 0) f" by simp

   443   thus

   444     "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>

   445      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"

   446     by simp

   447 next

   448   case (Suc n)

   449   hence "\<exists>a b.

   450    a < b \<and>

   451    newInt (Suc n) f = closed_int a b \<and>

   452    newInt (Suc n) f \<subseteq> newInt n f \<and>

   453    f (Suc n) \<notin> newInt (Suc n) f" by simp

   454   then obtain a and b where ab: "a < b \<and>

   455    newInt (Suc n) f = closed_int a b \<and>

   456    newInt (Suc n) f \<subseteq> newInt n f \<and>

   457    f (Suc n) \<notin> newInt (Suc n) f" by auto

   458   hence cab: "closed_int a b = newInt (Suc n) f" by simp

   459

   460   let ?e = "SOME e. \<exists>e1 e2.

   461     e1 < e2 \<and>

   462     e = closed_int e1 e2 \<and>

   463     e \<subseteq> closed_int a b \<and>

   464     f (Suc (Suc n)) \<notin> e"

   465   from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto

   466

   467   from ab have "a < b" by simp

   468   with closed_subset_ex have

   469     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>

   470      f (Suc (Suc n)) \<notin> closed_int ka kb" .

   471   hence

   472     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

   473      closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"

   474     by simp

   475   hence

   476     "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

   477      e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp

   478   hence

   479     "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>

   480      ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)

   481   with ab ni show

   482     "\<exists>ka kb. ka < kb \<and>

   483      newInt (Suc (Suc n)) f = closed_int ka kb \<and>

   484      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>

   485      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto

   486 qed

   487

   488 lemma newInt_subset:

   489   "newInt (Suc n) f \<subseteq> newInt n f"

   490   using newInt_ex by auto

   491

   492

   493 text {* Another fundamental property is that no element in the range

   494 of f is in the intersection of all closed intervals generated by

   495 newInt. *}

   496

   497 lemma newInt_inter:

   498   "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"

   499 proof

   500   fix n::nat

   501   {

   502     assume n0: "n = 0"

   503     moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp

   504     ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)

   505   }

   506   moreover

   507   {

   508     assume "\<not> n = 0"

   509     hence "n > 0" by simp

   510     then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)

   511

   512     from newInt_ex have

   513       "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>

   514        newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .

   515     then have "f (Suc m) \<notin> newInt (Suc m) f" by auto

   516     with ndef have "f n \<notin> newInt n f" by simp

   517   }

   518   ultimately have "f n \<notin> newInt n f" by (rule case_split)

   519   thus "f n \<notin> (\<Inter>n. newInt n f)" by auto

   520 qed

   521

   522

   523 lemma newInt_notempty:

   524   "(\<Inter>n. newInt n f) \<noteq> {}"

   525 proof -

   526   let ?g = "\<lambda>n. newInt n f"

   527   have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"

   528   proof

   529     fix n

   530     show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)

   531   qed

   532   moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"

   533   proof

   534     fix n::nat

   535     {

   536       assume "n = 0"

   537       then have

   538         "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"

   539         by simp

   540       hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast

   541     }

   542     moreover

   543     {

   544       assume "\<not> n = 0"

   545       then have "n > 0" by simp

   546       then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)

   547

   548       have

   549         "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>

   550         (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"

   551         by (rule newInt_ex)

   552       then obtain a and b where

   553         "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto

   554       with nd have "?g n = closed_int a b \<and> a \<le> b" by auto

   555       hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast

   556     }

   557     ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)

   558   qed

   559   ultimately show ?thesis by (rule NIP)

   560 qed

   561

   562

   563 subsection {* Final Theorem *}

   564

   565 theorem real_non_denum:

   566   shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"

   567 proof -- "by contradiction"

   568   assume "\<exists>f::nat\<Rightarrow>real. surj f"

   569   then obtain f::"nat\<Rightarrow>real" where "surj f" by auto

   570   hence rangeF: "range f = UNIV" by (rule surj_range)

   571   -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "

   572   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast

   573   moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)

   574   ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast

   575   moreover from rangeF have "x \<in> range f" by simp

   576   ultimately show False by blast

   577 qed

   578

   579 end