src/HOL/Library/ContNotDenum.thy
changeset 56796 9f84219715a7
parent 54797 be020ec8560c
child 57234 596a499318ab
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Apr 29 21:54:26 2014 +0200
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Tue Apr 29 22:50:55 2014 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4 -(*  Title       : HOL/ContNonDenum
     1.5 -    Author      : Benjamin Porter, Monash University, NICTA, 2005
     1.6 +(*  Title:      HOL/Library/ContNonDenum.thy
     1.7 +    Author:     Benjamin Porter, Monash University, NICTA, 2005
     1.8  *)
     1.9  
    1.10  header {* Non-denumerability of the Continuum. *}
    1.11 @@ -15,7 +15,7 @@
    1.12  system.
    1.13  
    1.14  {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
    1.15 -words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
    1.16 +words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
    1.17  surjective.
    1.18  
    1.19  {\em Outline:} An elegant informal proof of this result uses Cantor's
    1.20 @@ -25,41 +25,50 @@
    1.21  completeness of the Real numbers and is the foundation for our
    1.22  argument. Informally it states that an intersection of countable
    1.23  closed intervals (where each successive interval is a subset of the
    1.24 -last) is non-empty. We then assume a surjective function f:@{text
    1.25 -"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
    1.26 +last) is non-empty. We then assume a surjective function @{text
    1.27 +"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
    1.28  by generating a sequence of closed intervals then using the NIP. *}
    1.29  
    1.30 +
    1.31  subsection {* Closed Intervals *}
    1.32  
    1.33  subsection {* Nested Interval Property *}
    1.34  
    1.35  theorem NIP:
    1.36 -  fixes f::"nat \<Rightarrow> real set"
    1.37 +  fixes f :: "nat \<Rightarrow> real set"
    1.38    assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
    1.39 -  and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    1.40 +    and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    1.41    shows "(\<Inter>n. f n) \<noteq> {}"
    1.42  proof -
    1.43    let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
    1.44 -  { fix n 
    1.45 +  {
    1.46 +    fix n
    1.47      from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
    1.48        by auto
    1.49      then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
    1.50 -      by auto }
    1.51 +      by auto
    1.52 +  }
    1.53    note f_eq = this
    1.54 -  { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
    1.55 -      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
    1.56 +  {
    1.57 +    fix n m :: nat
    1.58 +    assume "n \<le> m"
    1.59 +    then have "f m \<subseteq> f n"
    1.60 +      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
    1.61 +  }
    1.62    note subset' = this
    1.63  
    1.64    have "compact (f 0)"
    1.65      by (subst f_eq) (rule compact_Icc)
    1.66    then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
    1.67    proof (rule compact_imp_fip_image)
    1.68 -    fix I :: "nat set" assume I: "finite I"
    1.69 +    fix I :: "nat set"
    1.70 +    assume I: "finite I"
    1.71      have "{} \<subset> f (Max (insert 0 I))"
    1.72        using f_eq[of "Max (insert 0 I)"] by auto
    1.73      also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
    1.74      proof (rule INF_greatest)
    1.75 -      fix i assume "i \<in> insert 0 I"
    1.76 +      fix i
    1.77 +      assume "i \<in> insert 0 I"
    1.78        with I show "f (Max (insert 0 I)) \<subseteq> f i"
    1.79          by (intro subset') auto
    1.80      qed
    1.81 @@ -70,6 +79,7 @@
    1.82      by auto
    1.83  qed
    1.84  
    1.85 +
    1.86  subsection {* Generating the intervals *}
    1.87  
    1.88  subsubsection {* Existence of non-singleton closed intervals *}
    1.89 @@ -80,7 +90,7 @@
    1.90  non-singleton itself. *}
    1.91  
    1.92  lemma closed_subset_ex:
    1.93 -  fixes c::real
    1.94 +  fixes c :: real
    1.95    assumes "a < b"
    1.96    shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
    1.97  proof (cases "c < b")
    1.98 @@ -90,39 +100,45 @@
    1.99      case True
   1.100      with `a < b` `c < b` have "c \<notin> {a..b}"
   1.101        by auto
   1.102 -    with `a < b` show ?thesis by auto
   1.103 +    with `a < b` show ?thesis
   1.104 +      by auto
   1.105    next
   1.106      case False
   1.107      then have "a \<le> c" by simp
   1.108      def ka \<equiv> "(c + b)/2"
   1.109 -
   1.110 -    from ka_def `c < b` have kalb: "ka < b" by auto
   1.111 -    moreover from ka_def `c < b` have kagc: "ka > c" by simp
   1.112 -    ultimately have "c\<notin>{ka..b}" by auto
   1.113 -    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
   1.114 -    hence "{ka..b} \<subseteq> {a..b}" by auto
   1.115 -    ultimately have
   1.116 -      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   1.117 -      using kalb by auto
   1.118 +    from ka_def `c < b` have "ka < b"
   1.119 +      by auto
   1.120 +    moreover from ka_def `c < b` have "ka > c"
   1.121 +      by simp
   1.122 +    ultimately have "c \<notin> {ka..b}"
   1.123 +      by auto
   1.124 +    moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
   1.125 +      by simp
   1.126 +    then have "{ka..b} \<subseteq> {a..b}"
   1.127 +      by auto
   1.128 +    ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   1.129 +      using `ka < b` by auto
   1.130      then show ?thesis
   1.131        by auto
   1.132    qed
   1.133  next
   1.134    case False
   1.135    then have "c \<ge> b" by simp
   1.136 -
   1.137    def kb \<equiv> "(a + b)/2"
   1.138    with `a < b` have "kb < b" by auto
   1.139 -  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
   1.140 +  with kb_def `c \<ge> b` have "a < kb" "kb < c"
   1.141 +    by auto
   1.142    from `kb < c` have c: "c \<notin> {a..kb}"
   1.143      by auto
   1.144    with `kb < b` have "{a..kb} \<subseteq> {a..b}"
   1.145      by auto
   1.146    with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
   1.147      by simp
   1.148 -  then show ?thesis by auto
   1.149 +  then show ?thesis
   1.150 +    by auto
   1.151  qed
   1.152  
   1.153 +
   1.154  subsection {* newInt: Interval generation *}
   1.155  
   1.156  text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
   1.157 @@ -130,17 +146,19 @@
   1.158  does not contain @{text "f (Suc n)"}. With the base case defined such
   1.159  that @{text "(f 0)\<notin>newInt 0 f"}. *}
   1.160  
   1.161 +
   1.162  subsubsection {* Definition *}
   1.163  
   1.164 -primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   1.165 +primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
   1.166 +where
   1.167    "newInt 0 f = {f 0 + 1..f 0 + 2}"
   1.168 -  | "newInt (Suc n) f =
   1.169 -      (SOME e. (\<exists>e1 e2.
   1.170 -       e1 < e2 \<and>
   1.171 -       e = {e1..e2} \<and>
   1.172 -       e \<subseteq> newInt n f \<and>
   1.173 -       f (Suc n) \<notin> e)
   1.174 -      )"
   1.175 +| "newInt (Suc n) f =
   1.176 +    (SOME e.
   1.177 +      (\<exists>e1 e2.
   1.178 +         e1 < e2 \<and>
   1.179 +         e = {e1..e2} \<and>
   1.180 +         e \<subseteq> newInt n f \<and>
   1.181 +         f (Suc n) \<notin> e))"
   1.182  
   1.183  
   1.184  subsubsection {* Properties *}
   1.185 @@ -150,81 +168,76 @@
   1.186  
   1.187  lemma newInt_ex:
   1.188    "\<exists>a b. a < b \<and>
   1.189 -   newInt (Suc n) f = {a..b} \<and>
   1.190 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.191 -   f (Suc n) \<notin> newInt (Suc n) f"
   1.192 +    newInt (Suc n) f = {a..b} \<and>
   1.193 +    newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.194 +    f (Suc n) \<notin> newInt (Suc n) f"
   1.195  proof (induct n)
   1.196    case 0
   1.197 -
   1.198    let ?e = "SOME e. \<exists>e1 e2.
   1.199 -   e1 < e2 \<and>
   1.200 -   e = {e1..e2} \<and>
   1.201 -   e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.202 -   f (Suc 0) \<notin> e"
   1.203 +    e1 < e2 \<and>
   1.204 +    e = {e1..e2} \<and>
   1.205 +    e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.206 +    f (Suc 0) \<notin> e"
   1.207  
   1.208    have "newInt (Suc 0) f = ?e" by auto
   1.209    moreover
   1.210    have "f 0 + 1 < f 0 + 2" by simp
   1.211 -  with closed_subset_ex have
   1.212 -    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.213 -     f (Suc 0) \<notin> {ka..kb}" .
   1.214 -  hence
   1.215 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.216 -     e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
   1.217 -  hence
   1.218 -    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   1.219 +  with closed_subset_ex
   1.220 +  have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
   1.221 +  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e"
   1.222 +    by simp
   1.223 +  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   1.224      by (rule someI_ex)
   1.225    ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   1.226 -   newInt (Suc 0) f = {e1..e2} \<and>
   1.227 -   newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.228 -   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   1.229 -  thus
   1.230 -    "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   1.231 -     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   1.232 +      newInt (Suc 0) f = {e1..e2} \<and>
   1.233 +      newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.234 +      f (Suc 0) \<notin> newInt (Suc 0) f"
   1.235 +    by simp
   1.236 +  then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   1.237 +      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   1.238      by simp
   1.239  next
   1.240    case (Suc n)
   1.241 -  hence "\<exists>a b.
   1.242 -   a < b \<and>
   1.243 -   newInt (Suc n) f = {a..b} \<and>
   1.244 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.245 -   f (Suc n) \<notin> newInt (Suc n) f" by simp
   1.246 +  then have "\<exists>a b.
   1.247 +      a < b \<and>
   1.248 +      newInt (Suc n) f = {a..b} \<and>
   1.249 +      newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.250 +      f (Suc n) \<notin> newInt (Suc n) f"
   1.251 +    by simp
   1.252    then obtain a and b where ab: "a < b \<and>
   1.253 -   newInt (Suc n) f = {a..b} \<and>
   1.254 -   newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.255 -   f (Suc n) \<notin> newInt (Suc n) f" by auto
   1.256 -  hence cab: "{a..b} = newInt (Suc n) f" by simp
   1.257 +      newInt (Suc n) f = {a..b} \<and>
   1.258 +      newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.259 +      f (Suc n) \<notin> newInt (Suc n) f"
   1.260 +    by auto
   1.261 +  then have cab: "{a..b} = newInt (Suc n) f"
   1.262 +    by simp
   1.263  
   1.264    let ?e = "SOME e. \<exists>e1 e2.
   1.265 -    e1 < e2 \<and>
   1.266 -    e = {e1..e2} \<and>
   1.267 -    e \<subseteq> {a..b} \<and>
   1.268 -    f (Suc (Suc n)) \<notin> e"
   1.269 -  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   1.270 +      e1 < e2 \<and>
   1.271 +      e = {e1..e2} \<and>
   1.272 +      e \<subseteq> {a..b} \<and>
   1.273 +      f (Suc (Suc n)) \<notin> e"
   1.274 +  from cab have ni: "newInt (Suc (Suc n)) f = ?e"
   1.275 +    by auto
   1.276  
   1.277    from ab have "a < b" by simp
   1.278 -  with closed_subset_ex have
   1.279 -    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   1.280 -     f (Suc (Suc n)) \<notin> {ka..kb}" .
   1.281 -  hence
   1.282 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.283 -     {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   1.284 +  with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   1.285 +    f (Suc (Suc n)) \<notin> {ka..kb}" .
   1.286 +  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.287 +      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   1.288 +    by simp
   1.289 +  then have "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e"
   1.290      by simp
   1.291 -  hence
   1.292 -    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.293 -     e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
   1.294 -  hence
   1.295 -    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
   1.296 -     ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   1.297 -  with ab ni show
   1.298 -    "\<exists>ka kb. ka < kb \<and>
   1.299 -     newInt (Suc (Suc n)) f = {ka..kb} \<and>
   1.300 -     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   1.301 -     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   1.302 +  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
   1.303 +    by (rule someI_ex)
   1.304 +  with ab ni show "\<exists>ka kb. ka < kb \<and>
   1.305 +      newInt (Suc (Suc n)) f = {ka..kb} \<and>
   1.306 +      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   1.307 +      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
   1.308 +    by auto
   1.309  qed
   1.310  
   1.311 -lemma newInt_subset:
   1.312 -  "newInt (Suc n) f \<subseteq> newInt n f"
   1.313 +lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
   1.314    using newInt_ex by auto
   1.315  
   1.316  
   1.317 @@ -232,34 +245,27 @@
   1.318  of f is in the intersection of all closed intervals generated by
   1.319  newInt. *}
   1.320  
   1.321 -lemma newInt_inter:
   1.322 -  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   1.323 +lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   1.324  proof
   1.325 -  fix n::nat
   1.326 -  {
   1.327 -    assume n0: "n = 0"
   1.328 -    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
   1.329 -    ultimately have "f n \<notin> newInt n f" by simp
   1.330 -  }
   1.331 -  moreover
   1.332 -  {
   1.333 -    assume "\<not> n = 0"
   1.334 -    hence "n > 0" by simp
   1.335 -    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   1.336 -
   1.337 -    from newInt_ex have
   1.338 -      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.339 -       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   1.340 -    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   1.341 -    with ndef have "f n \<notin> newInt n f" by simp
   1.342 -  }
   1.343 -  ultimately have "f n \<notin> newInt n f" by (rule case_split)
   1.344 -  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
   1.345 +  fix n :: nat
   1.346 +  have "f n \<notin> newInt n f"
   1.347 +  proof (cases n)
   1.348 +    case 0
   1.349 +    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
   1.350 +      by simp
   1.351 +    ultimately show ?thesis by simp
   1.352 +  next
   1.353 +    case (Suc m)
   1.354 +    from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.355 +      newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   1.356 +    then have "f (Suc m) \<notin> newInt (Suc m) f"
   1.357 +      by auto
   1.358 +    with Suc show ?thesis by simp
   1.359 +  qed
   1.360 +  then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
   1.361  qed
   1.362  
   1.363 -
   1.364 -lemma newInt_notempty:
   1.365 -  "(\<Inter>n. newInt n f) \<noteq> {}"
   1.366 +lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
   1.367  proof -
   1.368    let ?g = "\<lambda>n. newInt n f"
   1.369    have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
   1.370 @@ -269,30 +275,26 @@
   1.371    qed
   1.372    moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   1.373    proof
   1.374 -    fix n::nat
   1.375 -    {
   1.376 -      assume "n = 0"
   1.377 -      then have
   1.378 -        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   1.379 +    fix n :: nat
   1.380 +    show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   1.381 +    proof (cases n)
   1.382 +      case 0
   1.383 +      then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   1.384          by simp
   1.385 -      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   1.386 -    }
   1.387 -    moreover
   1.388 -    {
   1.389 -      assume "\<not> n = 0"
   1.390 -      then have "n > 0" by simp
   1.391 -      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   1.392 -
   1.393 -      have
   1.394 -        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.395 +      then show ?thesis
   1.396 +        by blast
   1.397 +    next
   1.398 +      case (Suc m)
   1.399 +      have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.400          (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   1.401          by (rule newInt_ex)
   1.402 -      then obtain a and b where
   1.403 -        "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
   1.404 -      with nd have "?g n = {a..b} \<and> a \<le> b" by auto
   1.405 -      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   1.406 -    }
   1.407 -    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
   1.408 +      then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
   1.409 +        by auto
   1.410 +      with Suc have "?g n = {a..b} \<and> a \<le> b"
   1.411 +        by auto
   1.412 +      then show ?thesis
   1.413 +        by blast
   1.414 +    qed
   1.415    qed
   1.416    ultimately show ?thesis by (rule NIP)
   1.417  qed
   1.418 @@ -300,17 +302,22 @@
   1.419  
   1.420  subsection {* Final Theorem *}
   1.421  
   1.422 -theorem real_non_denum:
   1.423 -  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
   1.424 -proof -- "by contradiction"
   1.425 -  assume "\<exists>f::nat\<Rightarrow>real. surj f"
   1.426 -  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
   1.427 -  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   1.428 -  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   1.429 -  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
   1.430 -  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
   1.431 -  moreover from rangeF have "x \<in> range f" by simp
   1.432 -  ultimately show False by blast
   1.433 +theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
   1.434 +proof
   1.435 +  assume "\<exists>f :: nat \<Rightarrow> real. surj f"
   1.436 +  then obtain f :: "nat \<Rightarrow> real" where "surj f"
   1.437 +    by auto
   1.438 +  txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
   1.439 +  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
   1.440 +    using newInt_notempty by blast
   1.441 +  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
   1.442 +    by (rule newInt_inter)
   1.443 +  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
   1.444 +    by blast
   1.445 +  moreover from `surj f` have "x \<in> range f"
   1.446 +    by simp
   1.447 +  ultimately show False
   1.448 +    by blast
   1.449  qed
   1.450  
   1.451  end