src/HOL/Library/ContNotDenum.thy
 author wenzelm Mon Sep 02 23:35:58 2013 +0200 (2013-09-02) changeset 53372 f5a6313c7fe4 parent 40702 cf26dd7395e4 child 54263 c4159fe6fa46 permissions -rw-r--r--
tuned proof;
     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 "a < b"

   327   shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"

   328 proof (cases "c < b")

   329   case True

   330   show ?thesis

   331   proof (cases "c < a")

   332     case True

   333     with a < b c < b have "c \<notin> closed_int a b"

   334       unfolding closed_int_def by auto

   335     with a < b show ?thesis by auto

   336   next

   337     case False

   338     then have "a \<le> c" by simp

   339     def ka \<equiv> "(c + b)/2"

   340

   341     from ka_def c < b have kalb: "ka < b" by auto

   342     moreover from ka_def c < b have kagc: "ka > c" by simp

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

   344     moreover from a \<le> c kagc have "ka \<ge> a" by simp

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

   346     ultimately have

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

   348       using kalb by auto

   349     then show ?thesis

   350       by auto

   351   qed

   352 next

   353   case False

   354   then have "c \<ge> b" by simp

   355

   356   def kb \<equiv> "(a + b)/2"

   357   with a < b have "kb < b" by auto

   358   with kb_def c \<ge> b have "a < kb" "kb < c" by auto

   359   from kb < c have c: "c \<notin> closed_int a kb"

   360     unfolding closed_int_def by auto

   361   with kb < b have "closed_int a kb \<subseteq> closed_int a b"

   362     unfolding closed_int_def by auto

   363   with a < kb c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"

   364     by simp

   365   then show ?thesis by auto

   366 qed

   367

   368 subsection {* newInt: Interval generation *}

   369

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

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

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

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

   374

   375 subsubsection {* Definition *}

   376

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

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

   379   | "newInt (Suc n) f =

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

   381        e1 < e2 \<and>

   382        e = closed_int e1 e2 \<and>

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

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

   385       )"

   386

   387

   388 subsubsection {* Properties *}

   389

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

   391 appropriate interval. *}

   392

   393 lemma newInt_ex:

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

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

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

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

   398 proof (induct n)

   399   case 0

   400

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

   402    e1 < e2 \<and>

   403    e = closed_int e1 e2 \<and>

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

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

   406

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

   408   moreover

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

   410   with closed_subset_ex have

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

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

   413   hence

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

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

   416   hence

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

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

   419     by (rule someI_ex)

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

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

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

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

   424   thus

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

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

   427     by simp

   428 next

   429   case (Suc n)

   430   hence "\<exists>a b.

   431    a < b \<and>

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

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

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

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

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

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

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

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

   440

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

   442     e1 < e2 \<and>

   443     e = closed_int e1 e2 \<and>

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

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

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

   447

   448   from ab have "a < b" by simp

   449   with closed_subset_ex have

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

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

   452   hence

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

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

   455     by simp

   456   hence

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

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

   459   hence

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

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

   462   with ab ni show

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

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

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

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

   467 qed

   468

   469 lemma newInt_subset:

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

   471   using newInt_ex by auto

   472

   473

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

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

   476 newInt. *}

   477

   478 lemma newInt_inter:

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

   480 proof

   481   fix n::nat

   482   {

   483     assume n0: "n = 0"

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

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

   486   }

   487   moreover

   488   {

   489     assume "\<not> n = 0"

   490     hence "n > 0" by simp

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

   492

   493     from newInt_ex have

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

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

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

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

   498   }

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

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

   501 qed

   502

   503

   504 lemma newInt_notempty:

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

   506 proof -

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

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

   509   proof

   510     fix n

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

   512   qed

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

   514   proof

   515     fix n::nat

   516     {

   517       assume "n = 0"

   518       then have

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

   520         by simp

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

   522     }

   523     moreover

   524     {

   525       assume "\<not> n = 0"

   526       then have "n > 0" by simp

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

   528

   529       have

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

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

   532         by (rule newInt_ex)

   533       then obtain a and b where

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

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

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

   537     }

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

   539   qed

   540   ultimately show ?thesis by (rule NIP)

   541 qed

   542

   543

   544 subsection {* Final Theorem *}

   545

   546 theorem real_non_denum:

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

   548 proof -- "by contradiction"

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

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

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

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

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

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

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

   556   ultimately show False by blast

   557 qed

   558

   559 end