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