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.10  header {* Non-denumerability of the Continuum. *}
1.11 @@ -15,7 +15,7 @@
1.12  system.
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.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.30 +
1.31  subsection {* Closed Intervals *}
1.33  subsection {* Nested Interval Property *}
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.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.85 +
1.86  subsection {* Generating the intervals *}
1.88  subsubsection {* Existence of non-singleton closed intervals *}
1.89 @@ -80,7 +90,7 @@
1.90  non-singleton itself. *}
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.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.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.154  subsection {* newInt: Interval generation *}
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.162  subsubsection {* Definition *}
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.184  subsubsection {* Properties *}
1.185 @@ -150,81 +168,76 @@
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.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.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.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.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.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.317 @@ -232,34 +245,27 @@
1.318  of f is in the intersection of all closed intervals generated by
1.319  newInt. *}
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.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.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.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.420  subsection {* Final Theorem *}
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.451  end