1 (* Title : HOL/Real/ContNonDenum |
|
2 ID : $Id$ |
|
3 Author : Benjamin Porter, Monash University, NICTA, 2005 |
|
4 *) |
|
5 |
|
6 header {* Non-denumerability of the Continuum. *} |
|
7 |
|
8 theory ContNotDenum |
|
9 imports RComplete "../Hilbert_Choice" |
|
10 begin |
|
11 |
|
12 subsection {* Abstract *} |
|
13 |
|
14 text {* The following document presents a proof that the Continuum is |
|
15 uncountable. It is formalised in the Isabelle/Isar theorem proving |
|
16 system. |
|
17 |
|
18 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other |
|
19 words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is |
|
20 surjective. |
|
21 |
|
22 {\em Outline:} An elegant informal proof of this result uses Cantor's |
|
23 Diagonalisation argument. The proof presented here is not this |
|
24 one. First we formalise some properties of closed intervals, then we |
|
25 prove the Nested Interval Property. This property relies on the |
|
26 completeness of the Real numbers and is the foundation for our |
|
27 argument. Informally it states that an intersection of countable |
|
28 closed intervals (where each successive interval is a subset of the |
|
29 last) is non-empty. We then assume a surjective function f:@{text |
|
30 "\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f |
|
31 by generating a sequence of closed intervals then using the NIP. *} |
|
32 |
|
33 subsection {* Closed Intervals *} |
|
34 |
|
35 text {* This section formalises some properties of closed intervals. *} |
|
36 |
|
37 subsubsection {* Definition *} |
|
38 |
|
39 definition |
|
40 closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where |
|
41 "closed_int x y = {z. x \<le> z \<and> z \<le> y}" |
|
42 |
|
43 subsubsection {* Properties *} |
|
44 |
|
45 lemma closed_int_subset: |
|
46 assumes xy: "x1 \<ge> x0" "y1 \<le> y0" |
|
47 shows "closed_int x1 y1 \<subseteq> closed_int x0 y0" |
|
48 proof - |
|
49 { |
|
50 fix x::real |
|
51 assume "x \<in> closed_int x1 y1" |
|
52 hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def) |
|
53 with xy have "x \<ge> x0 \<and> x \<le> y0" by auto |
|
54 hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def) |
|
55 } |
|
56 thus ?thesis by auto |
|
57 qed |
|
58 |
|
59 lemma closed_int_least: |
|
60 assumes a: "a \<le> b" |
|
61 shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)" |
|
62 proof |
|
63 from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp |
|
64 thus "a \<in> closed_int a b" by (unfold closed_int_def) |
|
65 next |
|
66 have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp |
|
67 thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def) |
|
68 qed |
|
69 |
|
70 lemma closed_int_most: |
|
71 assumes a: "a \<le> b" |
|
72 shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)" |
|
73 proof |
|
74 from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp |
|
75 thus "b \<in> closed_int a b" by (unfold closed_int_def) |
|
76 next |
|
77 have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp |
|
78 thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def) |
|
79 qed |
|
80 |
|
81 lemma closed_not_empty: |
|
82 shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" |
|
83 by (auto dest: closed_int_least) |
|
84 |
|
85 lemma closed_mem: |
|
86 assumes "a \<le> c" and "c \<le> b" |
|
87 shows "c \<in> closed_int a b" |
|
88 using assms unfolding closed_int_def by auto |
|
89 |
|
90 lemma closed_subset: |
|
91 assumes ac: "a \<le> b" "c \<le> d" |
|
92 assumes closed: "closed_int a b \<subseteq> closed_int c d" |
|
93 shows "b \<ge> c" |
|
94 proof - |
|
95 from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto |
|
96 hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto) |
|
97 with ac have "c\<le>b \<and> b\<le>d" by simp |
|
98 thus ?thesis by auto |
|
99 qed |
|
100 |
|
101 |
|
102 subsection {* Nested Interval Property *} |
|
103 |
|
104 theorem NIP: |
|
105 fixes f::"nat \<Rightarrow> real set" |
|
106 assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n" |
|
107 and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b" |
|
108 shows "(\<Inter>n. f n) \<noteq> {}" |
|
109 proof - |
|
110 let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))" |
|
111 have ne: "\<forall>n. \<exists>x. x\<in>(f n)" |
|
112 proof |
|
113 fix n |
|
114 from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp |
|
115 then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto |
|
116 hence "a \<le> b" .. |
|
117 with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp |
|
118 with fn show "\<exists>x. x\<in>(f n)" by simp |
|
119 qed |
|
120 |
|
121 have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" |
|
122 proof |
|
123 fix n |
|
124 from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" .. |
|
125 then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto |
|
126 hence "a \<le> b" by simp |
|
127 hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least) |
|
128 with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp |
|
129 hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" .. |
|
130 thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex) |
|
131 qed |
|
132 |
|
133 -- "A denotes the set of all left-most points of all the intervals ..." |
|
134 moreover obtain A where Adef: "A = ?g ` \<nat>" by simp |
|
135 ultimately have "\<exists>x. x\<in>A" |
|
136 proof - |
|
137 have "(0::nat) \<in> \<nat>" by simp |
|
138 moreover have "?g 0 = ?g 0" by simp |
|
139 ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI) |
|
140 with Adef have "?g 0 \<in> A" by simp |
|
141 thus ?thesis .. |
|
142 qed |
|
143 |
|
144 -- "Now show that A is bounded above ..." |
|
145 moreover have "\<exists>y. isUb (UNIV::real set) A y" |
|
146 proof - |
|
147 { |
|
148 fix n |
|
149 from ne have ex: "\<exists>x. x\<in>(f n)" .. |
|
150 from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp |
|
151 moreover |
|
152 from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" .. |
|
153 then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto |
|
154 hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast |
|
155 ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp |
|
156 with ex have "(?g n) \<le> b" by auto |
|
157 hence "\<exists>b. (?g n) \<le> b" by auto |
|
158 } |
|
159 hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" .. |
|
160 |
|
161 have fs: "\<forall>n::nat. f n \<subseteq> f 0" |
|
162 proof (rule allI, induct_tac n) |
|
163 show "f 0 \<subseteq> f 0" by simp |
|
164 next |
|
165 fix n |
|
166 assume "f n \<subseteq> f 0" |
|
167 moreover from subset have "f (Suc n) \<subseteq> f n" .. |
|
168 ultimately show "f (Suc n) \<subseteq> f 0" by simp |
|
169 qed |
|
170 have "\<forall>n. (?g n)\<in>(f 0)" |
|
171 proof |
|
172 fix n |
|
173 from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp |
|
174 hence "?g n \<in> f n" .. |
|
175 with fs show "?g n \<in> f 0" by auto |
|
176 qed |
|
177 moreover from closed |
|
178 obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast |
|
179 ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto |
|
180 with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast |
|
181 with Adef have "\<forall>y\<in>A. y\<le>b" by auto |
|
182 hence "A *<= b" by (unfold setle_def) |
|
183 moreover have "b \<in> (UNIV::real set)" by simp |
|
184 ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp |
|
185 hence "isUb (UNIV::real set) A b" by (unfold isUb_def) |
|
186 thus ?thesis by auto |
|
187 qed |
|
188 -- "by the Axiom Of Completeness, A has a least upper bound ..." |
|
189 ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete) |
|
190 |
|
191 -- "denote this least upper bound as t ..." |
|
192 then obtain t where tdef: "isLub UNIV A t" .. |
|
193 |
|
194 -- "and finally show that this least upper bound is in all the intervals..." |
|
195 have "\<forall>n. t \<in> f n" |
|
196 proof |
|
197 fix n::nat |
|
198 from closed obtain a and b where |
|
199 int: "f n = closed_int a b" and alb: "a \<le> b" by blast |
|
200 |
|
201 have "t \<ge> a" |
|
202 proof - |
|
203 have "a \<in> A" |
|
204 proof - |
|
205 (* by construction *) |
|
206 from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)" |
|
207 using closed_int_least by blast |
|
208 moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a" |
|
209 proof clarsimp |
|
210 fix e |
|
211 assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x" |
|
212 from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto |
|
213 |
|
214 from ein aux have "a \<le> e \<and> e \<le> e" by auto |
|
215 moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto |
|
216 ultimately show "e = a" by simp |
|
217 qed |
|
218 hence "\<And>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp |
|
219 ultimately have "(?g n) = a" by (rule some_equality) |
|
220 moreover |
|
221 { |
|
222 have "n = of_nat n" by simp |
|
223 moreover have "of_nat n \<in> \<nat>" by simp |
|
224 ultimately have "n \<in> \<nat>" |
|
225 apply - |
|
226 apply (subst(asm) eq_sym_conv) |
|
227 apply (erule subst) |
|
228 . |
|
229 } |
|
230 with Adef have "(?g n) \<in> A" by auto |
|
231 ultimately show ?thesis by simp |
|
232 qed |
|
233 with tdef show "a \<le> t" by (rule isLubD2) |
|
234 qed |
|
235 moreover have "t \<le> b" |
|
236 proof - |
|
237 have "isUb UNIV A b" |
|
238 proof - |
|
239 { |
|
240 from alb int have |
|
241 ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast |
|
242 |
|
243 have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n" |
|
244 proof (rule allI, induct_tac m) |
|
245 show "\<forall>n. f (n + 0) \<subseteq> f n" by simp |
|
246 next |
|
247 fix m n |
|
248 assume pp: "\<forall>p. f (p + n) \<subseteq> f p" |
|
249 { |
|
250 fix p |
|
251 from pp have "f (p + n) \<subseteq> f p" by simp |
|
252 moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto |
|
253 hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp |
|
254 ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp |
|
255 } |
|
256 thus "\<forall>p. f (p + Suc n) \<subseteq> f p" .. |
|
257 qed |
|
258 have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)" |
|
259 proof ((rule allI)+, rule impI) |
|
260 fix \<alpha>::nat and \<beta>::nat |
|
261 assume "\<beta> \<le> \<alpha>" |
|
262 hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add) |
|
263 then obtain k where "\<alpha> = \<beta> + k" .. |
|
264 moreover |
|
265 from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp |
|
266 ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto |
|
267 qed |
|
268 |
|
269 fix m |
|
270 { |
|
271 assume "m \<ge> n" |
|
272 with subsetm have "f m \<subseteq> f n" by simp |
|
273 with ain have "\<forall>x\<in>f m. x \<le> b" by auto |
|
274 moreover |
|
275 from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp |
|
276 ultimately have "?g m \<le> b" by auto |
|
277 } |
|
278 moreover |
|
279 { |
|
280 assume "\<not>(m \<ge> n)" |
|
281 hence "m < n" by simp |
|
282 with subsetm have sub: "(f n) \<subseteq> (f m)" by simp |
|
283 from closed obtain ma and mb where |
|
284 "f m = closed_int ma mb \<and> ma \<le> mb" by blast |
|
285 hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto |
|
286 from one alb sub fm int have "ma \<le> b" using closed_subset by blast |
|
287 moreover have "(?g m) = ma" |
|
288 proof - |
|
289 from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" .. |
|
290 moreover from one have |
|
291 "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)" |
|
292 by (rule closed_int_least) |
|
293 with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp |
|
294 ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto |
|
295 thus "?g m = ma" by auto |
|
296 qed |
|
297 ultimately have "?g m \<le> b" by simp |
|
298 } |
|
299 ultimately have "?g m \<le> b" by (rule case_split) |
|
300 } |
|
301 with Adef have "\<forall>y\<in>A. y\<le>b" by auto |
|
302 hence "A *<= b" by (unfold setle_def) |
|
303 moreover have "b \<in> (UNIV::real set)" by simp |
|
304 ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp |
|
305 thus "isUb (UNIV::real set) A b" by (unfold isUb_def) |
|
306 qed |
|
307 with tdef show "t \<le> b" by (rule isLub_le_isUb) |
|
308 qed |
|
309 ultimately have "t \<in> closed_int a b" by (rule closed_mem) |
|
310 with int show "t \<in> f n" by simp |
|
311 qed |
|
312 hence "t \<in> (\<Inter>n. f n)" by auto |
|
313 thus ?thesis by auto |
|
314 qed |
|
315 |
|
316 subsection {* Generating the intervals *} |
|
317 |
|
318 subsubsection {* Existence of non-singleton closed intervals *} |
|
319 |
|
320 text {* This lemma asserts that given any non-singleton closed |
|
321 interval (a,b) and any element c, there exists a closed interval that |
|
322 is a subset of (a,b) and that does not contain c and is a |
|
323 non-singleton itself. *} |
|
324 |
|
325 lemma closed_subset_ex: |
|
326 fixes c::real |
|
327 assumes alb: "a < b" |
|
328 shows |
|
329 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)" |
|
330 proof - |
|
331 { |
|
332 assume clb: "c < b" |
|
333 { |
|
334 assume cla: "c < a" |
|
335 from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto) |
|
336 with alb have |
|
337 "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b" |
|
338 by auto |
|
339 hence |
|
340 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)" |
|
341 by auto |
|
342 } |
|
343 moreover |
|
344 { |
|
345 assume ncla: "\<not>(c < a)" |
|
346 with clb have cdef: "a \<le> c \<and> c < b" by simp |
|
347 obtain ka where kadef: "ka = (c + b)/2" by blast |
|
348 |
|
349 from kadef clb have kalb: "ka < b" by auto |
|
350 moreover from kadef cdef have kagc: "ka > c" by simp |
|
351 ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto) |
|
352 moreover from cdef kagc have "ka \<ge> a" by simp |
|
353 hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto) |
|
354 ultimately have |
|
355 "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b" |
|
356 using kalb by auto |
|
357 hence |
|
358 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)" |
|
359 by auto |
|
360 |
|
361 } |
|
362 ultimately have |
|
363 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)" |
|
364 by (rule case_split) |
|
365 } |
|
366 moreover |
|
367 { |
|
368 assume "\<not> (c < b)" |
|
369 hence cgeb: "c \<ge> b" by simp |
|
370 |
|
371 obtain kb where kbdef: "kb = (a + b)/2" by blast |
|
372 with alb have kblb: "kb < b" by auto |
|
373 with kbdef cgeb have "a < kb \<and> kb < c" by auto |
|
374 moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto) |
|
375 moreover from kblb have |
|
376 "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto) |
|
377 ultimately have |
|
378 "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb" |
|
379 by simp |
|
380 hence |
|
381 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)" |
|
382 by auto |
|
383 } |
|
384 ultimately show ?thesis by (rule case_split) |
|
385 qed |
|
386 |
|
387 subsection {* newInt: Interval generation *} |
|
388 |
|
389 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a |
|
390 closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and |
|
391 does not contain @{text "f (Suc n)"}. With the base case defined such |
|
392 that @{text "(f 0)\<notin>newInt 0 f"}. *} |
|
393 |
|
394 subsubsection {* Definition *} |
|
395 |
|
396 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where |
|
397 "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" |
|
398 | "newInt (Suc n) f = |
|
399 (SOME e. (\<exists>e1 e2. |
|
400 e1 < e2 \<and> |
|
401 e = closed_int e1 e2 \<and> |
|
402 e \<subseteq> (newInt n f) \<and> |
|
403 (f (Suc n)) \<notin> e) |
|
404 )" |
|
405 |
|
406 declare newInt.simps [code del] |
|
407 |
|
408 subsubsection {* Properties *} |
|
409 |
|
410 text {* We now show that every application of newInt returns an |
|
411 appropriate interval. *} |
|
412 |
|
413 lemma newInt_ex: |
|
414 "\<exists>a b. a < b \<and> |
|
415 newInt (Suc n) f = closed_int a b \<and> |
|
416 newInt (Suc n) f \<subseteq> newInt n f \<and> |
|
417 f (Suc n) \<notin> newInt (Suc n) f" |
|
418 proof (induct n) |
|
419 case 0 |
|
420 |
|
421 let ?e = "SOME e. \<exists>e1 e2. |
|
422 e1 < e2 \<and> |
|
423 e = closed_int e1 e2 \<and> |
|
424 e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> |
|
425 f (Suc 0) \<notin> e" |
|
426 |
|
427 have "newInt (Suc 0) f = ?e" by auto |
|
428 moreover |
|
429 have "f 0 + 1 < f 0 + 2" by simp |
|
430 with closed_subset_ex have |
|
431 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> |
|
432 f (Suc 0) \<notin> (closed_int ka kb)" . |
|
433 hence |
|
434 "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and> |
|
435 e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp |
|
436 hence |
|
437 "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and> |
|
438 ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e" |
|
439 by (rule someI_ex) |
|
440 ultimately have "\<exists>e1 e2. e1 < e2 \<and> |
|
441 newInt (Suc 0) f = closed_int e1 e2 \<and> |
|
442 newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> |
|
443 f (Suc 0) \<notin> newInt (Suc 0) f" by simp |
|
444 thus |
|
445 "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and> |
|
446 newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f" |
|
447 by simp |
|
448 next |
|
449 case (Suc n) |
|
450 hence "\<exists>a b. |
|
451 a < b \<and> |
|
452 newInt (Suc n) f = closed_int a b \<and> |
|
453 newInt (Suc n) f \<subseteq> newInt n f \<and> |
|
454 f (Suc n) \<notin> newInt (Suc n) f" by simp |
|
455 then obtain a and b where ab: "a < b \<and> |
|
456 newInt (Suc n) f = closed_int a b \<and> |
|
457 newInt (Suc n) f \<subseteq> newInt n f \<and> |
|
458 f (Suc n) \<notin> newInt (Suc n) f" by auto |
|
459 hence cab: "closed_int a b = newInt (Suc n) f" by simp |
|
460 |
|
461 let ?e = "SOME e. \<exists>e1 e2. |
|
462 e1 < e2 \<and> |
|
463 e = closed_int e1 e2 \<and> |
|
464 e \<subseteq> closed_int a b \<and> |
|
465 f (Suc (Suc n)) \<notin> e" |
|
466 from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto |
|
467 |
|
468 from ab have "a < b" by simp |
|
469 with closed_subset_ex have |
|
470 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> |
|
471 f (Suc (Suc n)) \<notin> closed_int ka kb" . |
|
472 hence |
|
473 "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and> |
|
474 closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb" |
|
475 by simp |
|
476 hence |
|
477 "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and> |
|
478 e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp |
|
479 hence |
|
480 "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and> |
|
481 ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex) |
|
482 with ab ni show |
|
483 "\<exists>ka kb. ka < kb \<and> |
|
484 newInt (Suc (Suc n)) f = closed_int ka kb \<and> |
|
485 newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and> |
|
486 f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto |
|
487 qed |
|
488 |
|
489 lemma newInt_subset: |
|
490 "newInt (Suc n) f \<subseteq> newInt n f" |
|
491 using newInt_ex by auto |
|
492 |
|
493 |
|
494 text {* Another fundamental property is that no element in the range |
|
495 of f is in the intersection of all closed intervals generated by |
|
496 newInt. *} |
|
497 |
|
498 lemma newInt_inter: |
|
499 "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" |
|
500 proof |
|
501 fix n::nat |
|
502 { |
|
503 assume n0: "n = 0" |
|
504 moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp |
|
505 ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp) |
|
506 } |
|
507 moreover |
|
508 { |
|
509 assume "\<not> n = 0" |
|
510 hence "n > 0" by simp |
|
511 then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc) |
|
512 |
|
513 from newInt_ex have |
|
514 "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and> |
|
515 newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" . |
|
516 then have "f (Suc m) \<notin> newInt (Suc m) f" by auto |
|
517 with ndef have "f n \<notin> newInt n f" by simp |
|
518 } |
|
519 ultimately have "f n \<notin> newInt n f" by (rule case_split) |
|
520 thus "f n \<notin> (\<Inter>n. newInt n f)" by auto |
|
521 qed |
|
522 |
|
523 |
|
524 lemma newInt_notempty: |
|
525 "(\<Inter>n. newInt n f) \<noteq> {}" |
|
526 proof - |
|
527 let ?g = "\<lambda>n. newInt n f" |
|
528 have "\<forall>n. ?g (Suc n) \<subseteq> ?g n" |
|
529 proof |
|
530 fix n |
|
531 show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset) |
|
532 qed |
|
533 moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b" |
|
534 proof |
|
535 fix n::nat |
|
536 { |
|
537 assume "n = 0" |
|
538 then have |
|
539 "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)" |
|
540 by simp |
|
541 hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast |
|
542 } |
|
543 moreover |
|
544 { |
|
545 assume "\<not> n = 0" |
|
546 then have "n > 0" by simp |
|
547 then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc) |
|
548 |
|
549 have |
|
550 "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and> |
|
551 (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)" |
|
552 by (rule newInt_ex) |
|
553 then obtain a and b where |
|
554 "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto |
|
555 with nd have "?g n = closed_int a b \<and> a \<le> b" by auto |
|
556 hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast |
|
557 } |
|
558 ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split) |
|
559 qed |
|
560 ultimately show ?thesis by (rule NIP) |
|
561 qed |
|
562 |
|
563 |
|
564 subsection {* Final Theorem *} |
|
565 |
|
566 theorem real_non_denum: |
|
567 shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)" |
|
568 proof -- "by contradiction" |
|
569 assume "\<exists>f::nat\<Rightarrow>real. surj f" |
|
570 then obtain f::"nat\<Rightarrow>real" where "surj f" by auto |
|
571 hence rangeF: "range f = UNIV" by (rule surj_range) |
|
572 -- "We now produce a real number x that is not in the range of f, using the properties of newInt. " |
|
573 have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast |
|
574 moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter) |
|
575 ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast |
|
576 moreover from rangeF have "x \<in> range f" by simp |
|
577 ultimately show False by blast |
|
578 qed |
|
579 |
|
580 end |
|