(* Title : HOL/ContNonDenum
Author : Benjamin Porter, Monash University, NICTA, 2005
*)
header {* Non-denumerability of the Continuum. *}
theory ContNotDenum
imports Complex_Main
begin
subsection {* Abstract *}
text {* The following document presents a proof that the Continuum is
uncountable. It is formalised in the Isabelle/Isar theorem proving
system.
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
surjective.
{\em Outline:} An elegant informal proof of this result uses Cantor's
Diagonalisation argument. The proof presented here is not this
one. First we formalise some properties of closed intervals, then we
prove the Nested Interval Property. This property relies on the
completeness of the Real numbers and is the foundation for our
argument. Informally it states that an intersection of countable
closed intervals (where each successive interval is a subset of the
last) is non-empty. We then assume a surjective function f:@{text
"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
by generating a sequence of closed intervals then using the NIP. *}
subsection {* Closed Intervals *}
text {* This section formalises some properties of closed intervals. *}
subsubsection {* Definition *}
definition
closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
"closed_int x y = {z. x \<le> z \<and> z \<le> y}"
subsubsection {* Properties *}
lemma closed_int_subset:
assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
proof -
{
fix x::real
assume "x \<in> closed_int x1 y1"
hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
}
thus ?thesis by auto
qed
lemma closed_int_least:
assumes a: "a \<le> b"
shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
proof
from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
thus "a \<in> closed_int a b" by (unfold closed_int_def)
next
have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
qed
lemma closed_int_most:
assumes a: "a \<le> b"
shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
proof
from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
thus "b \<in> closed_int a b" by (unfold closed_int_def)
next
have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
qed
lemma closed_not_empty:
shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b"
by (auto dest: closed_int_least)
lemma closed_mem:
assumes "a \<le> c" and "c \<le> b"
shows "c \<in> closed_int a b"
using assms unfolding closed_int_def by auto
lemma closed_subset:
assumes ac: "a \<le> b" "c \<le> d"
assumes closed: "closed_int a b \<subseteq> closed_int c d"
shows "b \<ge> c"
proof -
from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
with ac have "c\<le>b \<and> b\<le>d" by simp
thus ?thesis by auto
qed
subsection {* Nested Interval Property *}
theorem NIP:
fixes f::"nat \<Rightarrow> real set"
assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
shows "(\<Inter>n. f n) \<noteq> {}"
proof -
let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
proof
fix n
from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
hence "a \<le> b" ..
with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
with fn show "\<exists>x. x\<in>(f n)" by simp
qed
have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
proof
fix n
from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
hence "a \<le> b" by simp
hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
qed
-- "A denotes the set of all left-most points of all the intervals ..."
moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
ultimately have "\<exists>x. x\<in>A"
proof -
have "(0::nat) \<in> \<nat>" by simp
moreover have "?g 0 = ?g 0" by simp
ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI)
with Adef have "?g 0 \<in> A" by simp
thus ?thesis ..
qed
-- "Now show that A is bounded above ..."
moreover have "\<exists>y. isUb (UNIV::real set) A y"
proof -
{
fix n
from ne have ex: "\<exists>x. x\<in>(f n)" ..
from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
moreover
from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
with ex have "(?g n) \<le> b" by auto
hence "\<exists>b. (?g n) \<le> b" by auto
}
hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
have fs: "\<forall>n::nat. f n \<subseteq> f 0"
proof (rule allI, induct_tac n)
show "f 0 \<subseteq> f 0" by simp
next
fix n
assume "f n \<subseteq> f 0"
moreover from subset have "f (Suc n) \<subseteq> f n" ..
ultimately show "f (Suc n) \<subseteq> f 0" by simp
qed
have "\<forall>n. (?g n)\<in>(f 0)"
proof
fix n
from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
hence "?g n \<in> f n" ..
with fs show "?g n \<in> f 0" by auto
qed
moreover from closed
obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
with Adef have "\<forall>y\<in>A. y\<le>b" by auto
hence "A *<= b" by (unfold setle_def)
moreover have "b \<in> (UNIV::real set)" by simp
ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
thus ?thesis by auto
qed
-- "by the Axiom Of Completeness, A has a least upper bound ..."
ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
-- "denote this least upper bound as t ..."
then obtain t where tdef: "isLub UNIV A t" ..
-- "and finally show that this least upper bound is in all the intervals..."
have "\<forall>n. t \<in> f n"
proof
fix n::nat
from closed obtain a and b where
int: "f n = closed_int a b" and alb: "a \<le> b" by blast
have "t \<ge> a"
proof -
have "a \<in> A"
proof -
(* by construction *)
from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
using closed_int_least by blast
moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
proof clarsimp
fix e
assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
from ein aux have "a \<le> e \<and> e \<le> e" by auto
moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
ultimately show "e = a" by simp
qed
hence "\<And>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
ultimately have "(?g n) = a" by (rule some_equality)
moreover
{
have "n = of_nat n" by simp
moreover have "of_nat n \<in> \<nat>" by simp
ultimately have "n \<in> \<nat>"
apply -
apply (subst(asm) eq_sym_conv)
apply (erule subst)
.
}
with Adef have "(?g n) \<in> A" by auto
ultimately show ?thesis by simp
qed
with tdef show "a \<le> t" by (rule isLubD2)
qed
moreover have "t \<le> b"
proof -
have "isUb UNIV A b"
proof -
{
from alb int have
ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
proof (rule allI, induct_tac m)
show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
next
fix m n
assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
{
fix p
from pp have "f (p + n) \<subseteq> f p" by simp
moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
}
thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
qed
have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
proof ((rule allI)+, rule impI)
fix \<alpha>::nat and \<beta>::nat
assume "\<beta> \<le> \<alpha>"
hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
then obtain k where "\<alpha> = \<beta> + k" ..
moreover
from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
qed
fix m
{
assume "m \<ge> n"
with subsetm have "f m \<subseteq> f n" by simp
with ain have "\<forall>x\<in>f m. x \<le> b" by auto
moreover
from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
ultimately have "?g m \<le> b" by auto
}
moreover
{
assume "\<not>(m \<ge> n)"
hence "m < n" by simp
with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
from closed obtain ma and mb where
"f m = closed_int ma mb \<and> ma \<le> mb" by blast
hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto
from one alb sub fm int have "ma \<le> b" using closed_subset by blast
moreover have "(?g m) = ma"
proof -
from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
moreover from one have
"ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
by (rule closed_int_least)
with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
thus "?g m = ma" by auto
qed
ultimately have "?g m \<le> b" by simp
}
ultimately have "?g m \<le> b" by (rule case_split)
}
with Adef have "\<forall>y\<in>A. y\<le>b" by auto
hence "A *<= b" by (unfold setle_def)
moreover have "b \<in> (UNIV::real set)" by simp
ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
qed
with tdef show "t \<le> b" by (rule isLub_le_isUb)
qed
ultimately have "t \<in> closed_int a b" by (rule closed_mem)
with int show "t \<in> f n" by simp
qed
hence "t \<in> (\<Inter>n. f n)" by auto
thus ?thesis by auto
qed
subsection {* Generating the intervals *}
subsubsection {* Existence of non-singleton closed intervals *}
text {* This lemma asserts that given any non-singleton closed
interval (a,b) and any element c, there exists a closed interval that
is a subset of (a,b) and that does not contain c and is a
non-singleton itself. *}
lemma closed_subset_ex:
fixes c::real
assumes alb: "a < b"
shows
"\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
proof -
{
assume clb: "c < b"
{
assume cla: "c < a"
from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
with alb have
"a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
by auto
hence
"\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
by auto
}
moreover
{
assume ncla: "\<not>(c < a)"
with clb have cdef: "a \<le> c \<and> c < b" by simp
obtain ka where kadef: "ka = (c + b)/2" by blast
from kadef clb have kalb: "ka < b" by auto
moreover from kadef cdef have kagc: "ka > c" by simp
ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
moreover from cdef kagc have "ka \<ge> a" by simp
hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
ultimately have
"ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
using kalb by auto
hence
"\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
by auto
}
ultimately have
"\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
by (rule case_split)
}
moreover
{
assume "\<not> (c < b)"
hence cgeb: "c \<ge> b" by simp
obtain kb where kbdef: "kb = (a + b)/2" by blast
with alb have kblb: "kb < b" by auto
with kbdef cgeb have "a < kb \<and> kb < c" by auto
moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
moreover from kblb have
"closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
ultimately have
"a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
by simp
hence
"\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
by auto
}
ultimately show ?thesis by (rule case_split)
qed
subsection {* newInt: Interval generation *}
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
does not contain @{text "f (Suc n)"}. With the base case defined such
that @{text "(f 0)\<notin>newInt 0 f"}. *}
subsubsection {* Definition *}
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
"newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
| "newInt (Suc n) f =
(SOME e. (\<exists>e1 e2.
e1 < e2 \<and>
e = closed_int e1 e2 \<and>
e \<subseteq> (newInt n f) \<and>
(f (Suc n)) \<notin> e)
)"
subsubsection {* Properties *}
text {* We now show that every application of newInt returns an
appropriate interval. *}
lemma newInt_ex:
"\<exists>a b. a < b \<and>
newInt (Suc n) f = closed_int a b \<and>
newInt (Suc n) f \<subseteq> newInt n f \<and>
f (Suc n) \<notin> newInt (Suc n) f"
proof (induct n)
case 0
let ?e = "SOME e. \<exists>e1 e2.
e1 < e2 \<and>
e = closed_int e1 e2 \<and>
e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
f (Suc 0) \<notin> e"
have "newInt (Suc 0) f = ?e" by auto
moreover
have "f 0 + 1 < f 0 + 2" by simp
with closed_subset_ex have
"\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
f (Suc 0) \<notin> (closed_int ka kb)" .
hence
"\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
hence
"\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
by (rule someI_ex)
ultimately have "\<exists>e1 e2. e1 < e2 \<and>
newInt (Suc 0) f = closed_int e1 e2 \<and>
newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
f (Suc 0) \<notin> newInt (Suc 0) f" by simp
thus
"\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
by simp
next
case (Suc n)
hence "\<exists>a b.
a < b \<and>
newInt (Suc n) f = closed_int a b \<and>
newInt (Suc n) f \<subseteq> newInt n f \<and>
f (Suc n) \<notin> newInt (Suc n) f" by simp
then obtain a and b where ab: "a < b \<and>
newInt (Suc n) f = closed_int a b \<and>
newInt (Suc n) f \<subseteq> newInt n f \<and>
f (Suc n) \<notin> newInt (Suc n) f" by auto
hence cab: "closed_int a b = newInt (Suc n) f" by simp
let ?e = "SOME e. \<exists>e1 e2.
e1 < e2 \<and>
e = closed_int e1 e2 \<and>
e \<subseteq> closed_int a b \<and>
f (Suc (Suc n)) \<notin> e"
from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
from ab have "a < b" by simp
with closed_subset_ex have
"\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
f (Suc (Suc n)) \<notin> closed_int ka kb" .
hence
"\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
by simp
hence
"\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
hence
"\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
with ab ni show
"\<exists>ka kb. ka < kb \<and>
newInt (Suc (Suc n)) f = closed_int ka kb \<and>
newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
qed
lemma newInt_subset:
"newInt (Suc n) f \<subseteq> newInt n f"
using newInt_ex by auto
text {* Another fundamental property is that no element in the range
of f is in the intersection of all closed intervals generated by
newInt. *}
lemma newInt_inter:
"\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
proof
fix n::nat
{
assume n0: "n = 0"
moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
}
moreover
{
assume "\<not> n = 0"
hence "n > 0" by simp
then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
from newInt_ex have
"\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
with ndef have "f n \<notin> newInt n f" by simp
}
ultimately have "f n \<notin> newInt n f" by (rule case_split)
thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
qed
lemma newInt_notempty:
"(\<Inter>n. newInt n f) \<noteq> {}"
proof -
let ?g = "\<lambda>n. newInt n f"
have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
proof
fix n
show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
qed
moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
proof
fix n::nat
{
assume "n = 0"
then have
"?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
by simp
hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
}
moreover
{
assume "\<not> n = 0"
then have "n > 0" by simp
then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
have
"\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
(newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
by (rule newInt_ex)
then obtain a and b where
"a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
}
ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
qed
ultimately show ?thesis by (rule NIP)
qed
subsection {* Final Theorem *}
theorem real_non_denum:
shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
proof -- "by contradiction"
assume "\<exists>f::nat\<Rightarrow>real. surj f"
then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
-- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
moreover from rangeF have "x \<in> range f" by simp
ultimately show False by blast
qed
end