src/HOL/Library/ContNotDenum.thy
 author chaieb Mon Feb 09 17:21:46 2009 +0000 (2009-02-09) changeset 29847 af32126ee729 parent 29026 5fbaa05f637f child 30663 0b6aff7451b2 permissions -rw-r--r--
     1 (*  Title       : HOL/ContNonDenum

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

     3 *)

     4

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

     6

     7 theory ContNotDenum

     8 imports RComplete Hilbert_Choice

     9 begin

    10

    11 subsection {* Abstract *}

    12

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

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

    15 system.

    16

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

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

    19 surjective.

    20

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

    22 Diagonalisation argument. The proof presented here is not this

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

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

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

    26 argument. Informally it states that an intersection of countable

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

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

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

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

    31

    32 subsection {* Closed Intervals *}

    33

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

    35

    36 subsubsection {* Definition *}

    37

    38 definition

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

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

    41

    42 subsubsection {* Properties *}

    43

    44 lemma closed_int_subset:

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

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

    47 proof -

    48   {

    49     fix x::real

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

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

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

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

    54   }

    55   thus ?thesis by auto

    56 qed

    57

    58 lemma closed_int_least:

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

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

    61 proof

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

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

    64 next

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

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

    67 qed

    68

    69 lemma closed_int_most:

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

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

    72 proof

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

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

    75 next

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

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

    78 qed

    79

    80 lemma closed_not_empty:

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

    82   by (auto dest: closed_int_least)

    83

    84 lemma closed_mem:

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

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

    87   using assms unfolding closed_int_def by auto

    88

    89 lemma closed_subset:

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

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

    92   shows "b \<ge> c"

    93 proof -

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

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

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

    97   thus ?thesis by auto

    98 qed

    99

   100

   101 subsection {* Nested Interval Property *}

   102

   103 theorem NIP:

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

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

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

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

   108 proof -

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

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

   111   proof

   112     fix n

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

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

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

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

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

   118   qed

   119

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

   121   proof

   122     fix n

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

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

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

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

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

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

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

   130   qed

   131

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

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

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

   135   proof -

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

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

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

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

   140     thus ?thesis ..

   141   qed

   142

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

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

   145   proof -

   146     {

   147       fix n

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

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

   150       moreover

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

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

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

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

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

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

   157     }

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

   159

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

   161     proof (rule allI, induct_tac n)

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

   163     next

   164       fix n

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

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

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

   168     qed

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

   170     proof

   171       fix n

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

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

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

   175     qed

   176     moreover from closed

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

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

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

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

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

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

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

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

   185     thus ?thesis by auto

   186   qed

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

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

   189

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

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

   192

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

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

   195   proof

   196     fix n::nat

   197     from closed obtain a and b where

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

   199

   200     have "t \<ge> a"

   201     proof -

   202       have "a \<in> A"

   203       proof -

   204           (* by construction *)

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

   206           using closed_int_least by blast

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

   208         proof clarsimp

   209           fix e

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

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

   212

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

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

   215           ultimately show "e = a" by simp

   216         qed

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

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

   219         moreover

   220         {

   221           have "n = of_nat n" by simp

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

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

   224             apply -

   225             apply (subst(asm) eq_sym_conv)

   226             apply (erule subst)

   227             .

   228         }

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

   230         ultimately show ?thesis by simp

   231       qed

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

   233     qed

   234     moreover have "t \<le> b"

   235     proof -

   236       have "isUb UNIV A b"

   237       proof -

   238         {

   239           from alb int have

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

   241

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

   243           proof (rule allI, induct_tac m)

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

   245           next

   246             fix m n

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

   248             {

   249               fix p

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

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

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

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

   254             }

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

   256           qed

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

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

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

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

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

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

   263             moreover

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

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

   266           qed

   267

   268           fix m

   269           {

   270             assume "m \<ge> n"

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

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

   273             moreover

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

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

   276           }

   277           moreover

   278           {

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

   280             hence "m < n" by simp

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

   282             from closed obtain ma and mb where

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

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

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

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

   287             proof -

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

   289               moreover from one have

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

   291                 by (rule closed_int_least)

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

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

   294               thus "?g m = ma" by auto

   295             qed

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

   297           }

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

   299         }

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

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

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

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

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

   305       qed

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

   307     qed

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

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

   310   qed

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

   312   thus ?thesis by auto

   313 qed

   314

   315 subsection {* Generating the intervals *}

   316

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

   318

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

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

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

   322 non-singleton itself. *}

   323

   324 lemma closed_subset_ex:

   325   fixes c::real

   326   assumes alb: "a < b"

   327   shows

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

   329 proof -

   330   {

   331     assume clb: "c < b"

   332     {

   333       assume cla: "c < a"

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

   335       with alb have

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

   337         by auto

   338       hence

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

   340         by auto

   341     }

   342     moreover

   343     {

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

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

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

   347

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

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

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

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

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

   353       ultimately have

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

   355         using kalb by auto

   356       hence

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

   358         by auto

   359

   360     }

   361     ultimately have

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

   363       by (rule case_split)

   364   }

   365   moreover

   366   {

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

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

   369

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

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

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

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

   374     moreover from kblb have

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

   376     ultimately have

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

   378       by simp

   379     hence

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

   381       by auto

   382   }

   383   ultimately show ?thesis by (rule case_split)

   384 qed

   385

   386 subsection {* newInt: Interval generation *}

   387

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

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

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

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

   392

   393 subsubsection {* Definition *}

   394

   395 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where

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

   397   | "newInt (Suc n) f =

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

   399        e1 < e2 \<and>

   400        e = closed_int e1 e2 \<and>

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

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

   403       )"

   404

   405 declare newInt.simps [code del]

   406

   407 subsubsection {* Properties *}

   408

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

   410 appropriate interval. *}

   411

   412 lemma newInt_ex:

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

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

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

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

   417 proof (induct n)

   418   case 0

   419

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

   421    e1 < e2 \<and>

   422    e = closed_int e1 e2 \<and>

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

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

   425

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

   427   moreover

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

   429   with closed_subset_ex have

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

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

   432   hence

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

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

   435   hence

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

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

   438     by (rule someI_ex)

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

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

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

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

   443   thus

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

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

   446     by simp

   447 next

   448   case (Suc n)

   449   hence "\<exists>a b.

   450    a < b \<and>

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

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

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

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

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

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

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

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

   459

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

   461     e1 < e2 \<and>

   462     e = closed_int e1 e2 \<and>

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

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

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

   466

   467   from ab have "a < b" by simp

   468   with closed_subset_ex have

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

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

   471   hence

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

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

   474     by simp

   475   hence

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

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

   478   hence

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

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

   481   with ab ni show

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

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

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

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

   486 qed

   487

   488 lemma newInt_subset:

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

   490   using newInt_ex by auto

   491

   492

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

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

   495 newInt. *}

   496

   497 lemma newInt_inter:

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

   499 proof

   500   fix n::nat

   501   {

   502     assume n0: "n = 0"

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

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

   505   }

   506   moreover

   507   {

   508     assume "\<not> n = 0"

   509     hence "n > 0" by simp

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

   511

   512     from newInt_ex have

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

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

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

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

   517   }

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

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

   520 qed

   521

   522

   523 lemma newInt_notempty:

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

   525 proof -

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

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

   528   proof

   529     fix n

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

   531   qed

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

   533   proof

   534     fix n::nat

   535     {

   536       assume "n = 0"

   537       then have

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

   539         by simp

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

   541     }

   542     moreover

   543     {

   544       assume "\<not> n = 0"

   545       then have "n > 0" by simp

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

   547

   548       have

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

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

   551         by (rule newInt_ex)

   552       then obtain a and b where

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

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

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

   556     }

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

   558   qed

   559   ultimately show ?thesis by (rule NIP)

   560 qed

   561

   562

   563 subsection {* Final Theorem *}

   564

   565 theorem real_non_denum:

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

   567 proof -- "by contradiction"

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

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

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

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

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

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

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

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

   576   ultimately show False by blast

   577 qed

   578

   579 end