src/HOL/Library/ContNotDenum.thy
 author bulwahn Fri Apr 08 16:31:14 2011 +0200 (2011-04-08) changeset 42316 12635bb655fd parent 40702 cf26dd7395e4 child 53372 f5a6313c7fe4 permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
1 (*  Title       : HOL/ContNonDenum
2     Author      : Benjamin Porter, Monash University, NICTA, 2005
3 *)
5 header {* Non-denumerability of the Continuum. *}
7 theory ContNotDenum
8 imports Complex_Main
9 begin
11 subsection {* Abstract *}
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.
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.
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. *}
32 subsection {* Closed Intervals *}
34 text {* This section formalises some properties of closed intervals. *}
36 subsubsection {* Definition *}
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}"
42 subsubsection {* Properties *}
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
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
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
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)
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
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
101 subsection {* Nested Interval Property *}
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
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
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
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" ..
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)
190   -- "denote this least upper bound as t ..."
191   then obtain t where tdef: "isLub UNIV A t" ..
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
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
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
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
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
315 subsection {* Generating the intervals *}
317 subsubsection {* Existence of non-singleton closed intervals *}
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. *}
324 lemma closed_subset_ex:
325   fixes c::real
326   assumes alb: "a < b"
327   shows
328     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
329 proof -
330   {
331     assume clb: "c < b"
332     {
333       assume cla: "c < a"
334       from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
335       with alb have
336         "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
337         by auto
338       hence
339         "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
340         by auto
341     }
342     moreover
343     {
344       assume ncla: "\<not>(c < a)"
345       with clb have cdef: "a \<le> c \<and> c < b" by simp
346       obtain ka where kadef: "ka = (c + b)/2" by blast
348       from kadef clb have kalb: "ka < b" by auto
349       moreover from kadef cdef have kagc: "ka > c" by simp
350       ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
351       moreover from cdef kagc have "ka \<ge> a" by simp
352       hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
353       ultimately have
354         "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
355         using kalb by auto
356       hence
357         "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
358         by auto
360     }
361     ultimately have
362       "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
363       by (rule case_split)
364   }
365   moreover
366   {
367     assume "\<not> (c < b)"
368     hence cgeb: "c \<ge> b" by simp
370     obtain kb where kbdef: "kb = (a + b)/2" by blast
371     with alb have kblb: "kb < b" by auto
372     with kbdef cgeb have "a < kb \<and> kb < c" by auto
373     moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
374     moreover from kblb have
375       "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
376     ultimately have
377       "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
378       by simp
379     hence
380       "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
381       by auto
382   }
383   ultimately show ?thesis by (rule case_split)
384 qed
386 subsection {* newInt: Interval generation *}
388 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
389 closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
390 does not contain @{text "f (Suc n)"}. With the base case defined such
391 that @{text "(f 0)\<notin>newInt 0 f"}. *}
393 subsubsection {* Definition *}
395 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
396   "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
397   | "newInt (Suc n) f =
398       (SOME e. (\<exists>e1 e2.
399        e1 < e2 \<and>
400        e = closed_int e1 e2 \<and>
401        e \<subseteq> (newInt n f) \<and>
402        (f (Suc n)) \<notin> e)
403       )"
406 subsubsection {* Properties *}
408 text {* We now show that every application of newInt returns an
409 appropriate interval. *}
411 lemma newInt_ex:
412   "\<exists>a b. a < b \<and>
413    newInt (Suc n) f = closed_int a b \<and>
414    newInt (Suc n) f \<subseteq> newInt n f \<and>
415    f (Suc n) \<notin> newInt (Suc n) f"
416 proof (induct n)
417   case 0
419   let ?e = "SOME e. \<exists>e1 e2.
420    e1 < e2 \<and>
421    e = closed_int e1 e2 \<and>
422    e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
423    f (Suc 0) \<notin> e"
425   have "newInt (Suc 0) f = ?e" by auto
426   moreover
427   have "f 0 + 1 < f 0 + 2" by simp
428   with closed_subset_ex have
429     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
430      f (Suc 0) \<notin> (closed_int ka kb)" .
431   hence
432     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
433      e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
434   hence
435     "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
436      ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
437     by (rule someI_ex)
438   ultimately have "\<exists>e1 e2. e1 < e2 \<and>
439    newInt (Suc 0) f = closed_int e1 e2 \<and>
440    newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
441    f (Suc 0) \<notin> newInt (Suc 0) f" by simp
442   thus
443     "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
444      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
445     by simp
446 next
447   case (Suc n)
448   hence "\<exists>a b.
449    a < b \<and>
450    newInt (Suc n) f = closed_int a b \<and>
451    newInt (Suc n) f \<subseteq> newInt n f \<and>
452    f (Suc n) \<notin> newInt (Suc n) f" by simp
453   then obtain a and b where ab: "a < b \<and>
454    newInt (Suc n) f = closed_int a b \<and>
455    newInt (Suc n) f \<subseteq> newInt n f \<and>
456    f (Suc n) \<notin> newInt (Suc n) f" by auto
457   hence cab: "closed_int a b = newInt (Suc n) f" by simp
459   let ?e = "SOME e. \<exists>e1 e2.
460     e1 < e2 \<and>
461     e = closed_int e1 e2 \<and>
462     e \<subseteq> closed_int a b \<and>
463     f (Suc (Suc n)) \<notin> e"
464   from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
466   from ab have "a < b" by simp
467   with closed_subset_ex have
468     "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
469      f (Suc (Suc n)) \<notin> closed_int ka kb" .
470   hence
471     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
472      closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
473     by simp
474   hence
475     "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
476      e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
477   hence
478     "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
479      ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
480   with ab ni show
481     "\<exists>ka kb. ka < kb \<and>
482      newInt (Suc (Suc n)) f = closed_int ka kb \<and>
483      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
484      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
485 qed
487 lemma newInt_subset:
488   "newInt (Suc n) f \<subseteq> newInt n f"
489   using newInt_ex by auto
492 text {* Another fundamental property is that no element in the range
493 of f is in the intersection of all closed intervals generated by
494 newInt. *}
496 lemma newInt_inter:
497   "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
498 proof
499   fix n::nat
500   {
501     assume n0: "n = 0"
502     moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
503     ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
504   }
505   moreover
506   {
507     assume "\<not> n = 0"
508     hence "n > 0" by simp
509     then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
511     from newInt_ex have
512       "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
513        newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
514     then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
515     with ndef have "f n \<notin> newInt n f" by simp
516   }
517   ultimately have "f n \<notin> newInt n f" by (rule case_split)
518   thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
519 qed
522 lemma newInt_notempty:
523   "(\<Inter>n. newInt n f) \<noteq> {}"
524 proof -
525   let ?g = "\<lambda>n. newInt n f"
526   have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
527   proof
528     fix n
529     show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
530   qed
531   moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
532   proof
533     fix n::nat
534     {
535       assume "n = 0"
536       then have
537         "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
538         by simp
539       hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
540     }
541     moreover
542     {
543       assume "\<not> n = 0"
544       then have "n > 0" by simp
545       then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
547       have
548         "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
549         (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
550         by (rule newInt_ex)
551       then obtain a and b where
552         "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
553       with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
554       hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
555     }
556     ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
557   qed
558   ultimately show ?thesis by (rule NIP)
559 qed
562 subsection {* Final Theorem *}
564 theorem real_non_denum:
565   shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
566 proof -- "by contradiction"
567   assume "\<exists>f::nat\<Rightarrow>real. surj f"
568   then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
569   -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
570   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
571   moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
572   ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
573   moreover from rangeF have "x \<in> range f" by simp
574   ultimately show False by blast
575 qed
577 end