src/HOL/Library/ContNotDenum.thy
 author haftmann Fri Aug 27 19:34:23 2010 +0200 (2010-08-27 ago) changeset 38857 97775f3e8722 parent 37765 26bdfb7b680b child 40702 cf26dd7395e4 permissions -rw-r--r--
renamed class/constant eq to equal; tuned some instantiations
     1 (*  Title       : HOL/ContNonDenum

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

     3 *)

     4

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

     6

     7 theory ContNotDenum

     8 imports Complex_Main

     9 begin

    10

    11 subsection {* Abstract *}

    12

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

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

    15 system.

    16

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

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

    19 surjective.

    20

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

    22 Diagonalisation argument. The proof presented here is not this

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

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

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

    26 argument. Informally it states that an intersection of countable

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

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

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

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

    31

    32 subsection {* Closed Intervals *}

    33

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

    35

    36 subsubsection {* Definition *}

    37

    38 definition

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

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

    41

    42 subsubsection {* Properties *}

    43

    44 lemma closed_int_subset:

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

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

    47 proof -

    48   {

    49     fix x::real

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

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

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

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

    54   }

    55   thus ?thesis by auto

    56 qed

    57

    58 lemma closed_int_least:

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

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

    61 proof

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

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

    64 next

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

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

    67 qed

    68

    69 lemma closed_int_most:

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

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

    72 proof

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

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

    75 next

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

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

    78 qed

    79

    80 lemma closed_not_empty:

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

    82   by (auto dest: closed_int_least)

    83

    84 lemma closed_mem:

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

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

    87   using assms unfolding closed_int_def by auto

    88

    89 lemma closed_subset:

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

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

    92   shows "b \<ge> c"

    93 proof -

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

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

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

    97   thus ?thesis by auto

    98 qed

    99

   100

   101 subsection {* Nested Interval Property *}

   102

   103 theorem NIP:

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

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

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

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

   108 proof -

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

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

   111   proof

   112     fix n

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

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

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

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

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

   118   qed

   119

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

   121   proof

   122     fix n

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

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

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

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

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

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

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

   130   qed

   131

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

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

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

   135   proof -

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

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

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

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

   140     thus ?thesis ..

   141   qed

   142

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

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

   145   proof -

   146     {

   147       fix n

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

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

   150       moreover

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

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

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

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

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

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

   157     }

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

   159

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

   161     proof (rule allI, induct_tac n)

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

   163     next

   164       fix n

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

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

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

   168     qed

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

   170     proof

   171       fix n

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

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

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

   175     qed

   176     moreover from closed

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

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

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

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

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

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

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

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

   185     thus ?thesis by auto

   186   qed

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

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

   189

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

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

   192

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

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

   195   proof

   196     fix n::nat

   197     from closed obtain a and b where

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

   199

   200     have "t \<ge> a"

   201     proof -

   202       have "a \<in> A"

   203       proof -

   204           (* by construction *)

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

   206           using closed_int_least by blast

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

   208         proof clarsimp

   209           fix e

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

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

   212

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

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

   215           ultimately show "e = a" by simp

   216         qed

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

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

   219         moreover

   220         {

   221           have "n = of_nat n" by simp

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

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

   224             apply -

   225             apply (subst(asm) eq_sym_conv)

   226             apply (erule subst)

   227             .

   228         }

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

   230         ultimately show ?thesis by simp

   231       qed

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

   233     qed

   234     moreover have "t \<le> b"

   235     proof -

   236       have "isUb UNIV A b"

   237       proof -

   238         {

   239           from alb int have

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

   241

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

   243           proof (rule allI, induct_tac m)

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

   245           next

   246             fix m n

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

   248             {

   249               fix p

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

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

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

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

   254             }

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

   256           qed

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

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

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

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

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

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

   263             moreover

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

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

   266           qed

   267

   268           fix m

   269           {

   270             assume "m \<ge> n"

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

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

   273             moreover

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

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

   276           }

   277           moreover

   278           {

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

   280             hence "m < n" by simp

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

   282             from closed obtain ma and mb where

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

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

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

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

   287             proof -

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

   289               moreover from one have

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

   291                 by (rule closed_int_least)

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

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

   294               thus "?g m = ma" by auto

   295             qed

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

   297           }

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

   299         }

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

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

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

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

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

   305       qed

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

   307     qed

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

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

   310   qed

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

   312   thus ?thesis by auto

   313 qed

   314

   315 subsection {* Generating the intervals *}

   316

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

   318

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

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

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

   322 non-singleton itself. *}

   323

   324 lemma closed_subset_ex:

   325   fixes c::real

   326   assumes alb: "a < b"

   327   shows

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

   329 proof -

   330   {

   331     assume clb: "c < b"

   332     {

   333       assume cla: "c < a"

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

   335       with alb have

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

   337         by auto

   338       hence

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

   340         by auto

   341     }

   342     moreover

   343     {

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

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

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

   347

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

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

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

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

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

   353       ultimately have

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

   355         using kalb by auto

   356       hence

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

   358         by auto

   359

   360     }

   361     ultimately have

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

   363       by (rule case_split)

   364   }

   365   moreover

   366   {

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

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

   369

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

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

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

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

   374     moreover from kblb have

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

   376     ultimately have

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

   378       by simp

   379     hence

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

   381       by auto

   382   }

   383   ultimately show ?thesis by (rule case_split)

   384 qed

   385

   386 subsection {* newInt: Interval generation *}

   387

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

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

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

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

   392

   393 subsubsection {* Definition *}

   394

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

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

   397   | "newInt (Suc n) f =

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

   399        e1 < e2 \<and>

   400        e = closed_int e1 e2 \<and>

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

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

   403       )"

   404

   405

   406 subsubsection {* Properties *}

   407

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

   409 appropriate interval. *}

   410

   411 lemma newInt_ex:

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

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

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

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

   416 proof (induct n)

   417   case 0

   418

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

   420    e1 < e2 \<and>

   421    e = closed_int e1 e2 \<and>

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

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

   424

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

   426   moreover

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

   428   with closed_subset_ex have

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

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

   431   hence

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

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

   434   hence

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

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

   437     by (rule someI_ex)

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

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

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

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

   442   thus

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

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

   445     by simp

   446 next

   447   case (Suc n)

   448   hence "\<exists>a b.

   449    a < b \<and>

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

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

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

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

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

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

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

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

   458

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

   460     e1 < e2 \<and>

   461     e = closed_int e1 e2 \<and>

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

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

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

   465

   466   from ab have "a < b" by simp

   467   with closed_subset_ex have

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

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

   470   hence

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

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

   473     by simp

   474   hence

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

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

   477   hence

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

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

   480   with ab ni show

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

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

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

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

   485 qed

   486

   487 lemma newInt_subset:

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

   489   using newInt_ex by auto

   490

   491

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

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

   494 newInt. *}

   495

   496 lemma newInt_inter:

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

   498 proof

   499   fix n::nat

   500   {

   501     assume n0: "n = 0"

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

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

   504   }

   505   moreover

   506   {

   507     assume "\<not> n = 0"

   508     hence "n > 0" by simp

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

   510

   511     from newInt_ex have

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

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

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

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

   516   }

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

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

   519 qed

   520

   521

   522 lemma newInt_notempty:

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

   524 proof -

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

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

   527   proof

   528     fix n

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

   530   qed

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

   532   proof

   533     fix n::nat

   534     {

   535       assume "n = 0"

   536       then have

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

   538         by simp

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

   540     }

   541     moreover

   542     {

   543       assume "\<not> n = 0"

   544       then have "n > 0" by simp

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

   546

   547       have

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

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

   550         by (rule newInt_ex)

   551       then obtain a and b where

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

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

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

   555     }

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

   557   qed

   558   ultimately show ?thesis by (rule NIP)

   559 qed

   560

   561

   562 subsection {* Final Theorem *}

   563

   564 theorem real_non_denum:

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

   566 proof -- "by contradiction"

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

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

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

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

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

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

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

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

   575   ultimately show False by blast

   576 qed

   577

   578 end