summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/ContNotDenum.thy

author | hoelzl |

Tue Nov 05 09:45:02 2013 +0100 (2013-11-05) | |

changeset 54263 | c4159fe6fa46 |

parent 53372 | f5a6313c7fe4 |

child 54797 | be020ec8560c |

permissions | -rw-r--r-- |

move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

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 "A \<noteq> {}"

135 proof -

136 have "(0::nat) \<in> \<nat>" by simp

137 with Adef show ?thesis

138 by blast

139 qed

141 -- "Now show that A is bounded above ..."

142 moreover have "bdd_above A"

143 proof -

144 {

145 fix n

146 from ne have ex: "\<exists>x. x\<in>(f n)" ..

147 from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp

148 moreover

149 from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..

150 then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto

151 hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast

152 ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp

153 with ex have "(?g n) \<le> b" by auto

154 hence "\<exists>b. (?g n) \<le> b" by auto

155 }

156 hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..

158 have fs: "\<forall>n::nat. f n \<subseteq> f 0"

159 proof (rule allI, induct_tac n)

160 show "f 0 \<subseteq> f 0" by simp

161 next

162 fix n

163 assume "f n \<subseteq> f 0"

164 moreover from subset have "f (Suc n) \<subseteq> f n" ..

165 ultimately show "f (Suc n) \<subseteq> f 0" by simp

166 qed

167 have "\<forall>n. (?g n)\<in>(f 0)"

168 proof

169 fix n

170 from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp

171 hence "?g n \<in> f n" ..

172 with fs show "?g n \<in> f 0" by auto

173 qed

174 moreover from closed

175 obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast

176 ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto

177 with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast

178 with Adef show "bdd_above A" by auto

179 qed

181 -- "denote this least upper bound as t ..."

182 def tdef: t == "Sup A"

184 -- "and finally show that this least upper bound is in all the intervals..."

185 have "\<forall>n. t \<in> f n"

186 proof

187 fix n::nat

188 from closed obtain a and b where

189 int: "f n = closed_int a b" and alb: "a \<le> b" by blast

191 have "t \<ge> a"

192 proof -

193 have "a \<in> A"

194 proof -

195 (* by construction *)

196 from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"

197 using closed_int_least by blast

198 moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"

199 proof clarsimp

200 fix e

201 assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"

202 from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto

204 from ein aux have "a \<le> e \<and> e \<le> e" by auto

205 moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto

206 ultimately show "e = a" by simp

207 qed

208 hence "\<And>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp

209 ultimately have "(?g n) = a" by (rule some_equality)

210 moreover

211 {

212 have "n = of_nat n" by simp

213 moreover have "of_nat n \<in> \<nat>" by simp

214 ultimately have "n \<in> \<nat>"

215 apply -

216 apply (subst(asm) eq_sym_conv)

217 apply (erule subst)

218 .

219 }

220 with Adef have "(?g n) \<in> A" by auto

221 ultimately show ?thesis by simp

222 qed

223 with `bdd_above A` show "a \<le> t"

224 unfolding tdef by (intro cSup_upper)

225 qed

226 moreover have "t \<le> b"

227 unfolding tdef

228 proof (rule cSup_least)

229 {

230 from alb int have

231 ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast

233 have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"

234 proof (rule allI, induct_tac m)

235 show "\<forall>n. f (n + 0) \<subseteq> f n" by simp

236 next

237 fix m n

238 assume pp: "\<forall>p. f (p + n) \<subseteq> f p"

239 {

240 fix p

241 from pp have "f (p + n) \<subseteq> f p" by simp

242 moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto

243 hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp

244 ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp

245 }

246 thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..

247 qed

248 have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"

249 proof ((rule allI)+, rule impI)

250 fix \<alpha>::nat and \<beta>::nat

251 assume "\<beta> \<le> \<alpha>"

252 hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)

253 then obtain k where "\<alpha> = \<beta> + k" ..

254 moreover

255 from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp

256 ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto

257 qed

259 fix m

260 {

261 assume "m \<ge> n"

262 with subsetm have "f m \<subseteq> f n" by simp

263 with ain have "\<forall>x\<in>f m. x \<le> b" by auto

264 moreover

265 from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp

266 ultimately have "?g m \<le> b" by auto

267 }

268 moreover

269 {

270 assume "\<not>(m \<ge> n)"

271 hence "m < n" by simp

272 with subsetm have sub: "(f n) \<subseteq> (f m)" by simp

273 from closed obtain ma and mb where

274 "f m = closed_int ma mb \<and> ma \<le> mb" by blast

275 hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto

276 from one alb sub fm int have "ma \<le> b" using closed_subset by blast

277 moreover have "(?g m) = ma"

278 proof -

279 from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..

280 moreover from one have

281 "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"

282 by (rule closed_int_least)

283 with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp

284 ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto

285 thus "?g m = ma" by auto

286 qed

287 ultimately have "?g m \<le> b" by simp

288 }

289 ultimately have "?g m \<le> b" by (rule case_split)

290 }

291 with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto

292 qed fact

293 ultimately have "t \<in> closed_int a b" by (rule closed_mem)

294 with int show "t \<in> f n" by simp

295 qed

296 hence "t \<in> (\<Inter>n. f n)" by auto

297 thus ?thesis by auto

298 qed

300 subsection {* Generating the intervals *}

302 subsubsection {* Existence of non-singleton closed intervals *}

304 text {* This lemma asserts that given any non-singleton closed

305 interval (a,b) and any element c, there exists a closed interval that

306 is a subset of (a,b) and that does not contain c and is a

307 non-singleton itself. *}

309 lemma closed_subset_ex:

310 fixes c::real

311 assumes "a < b"

312 shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"

313 proof (cases "c < b")

314 case True

315 show ?thesis

316 proof (cases "c < a")

317 case True

318 with `a < b` `c < b` have "c \<notin> closed_int a b"

319 unfolding closed_int_def by auto

320 with `a < b` show ?thesis by auto

321 next

322 case False

323 then have "a \<le> c" by simp

324 def ka \<equiv> "(c + b)/2"

326 from ka_def `c < b` have kalb: "ka < b" by auto

327 moreover from ka_def `c < b` have kagc: "ka > c" by simp

328 ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)

329 moreover from `a \<le> c` kagc have "ka \<ge> a" by simp

330 hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)

331 ultimately have

332 "ka < b \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"

333 using kalb by auto

334 then show ?thesis

335 by auto

336 qed

337 next

338 case False

339 then have "c \<ge> b" by simp

341 def kb \<equiv> "(a + b)/2"

342 with `a < b` have "kb < b" by auto

343 with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto

344 from `kb < c` have c: "c \<notin> closed_int a kb"

345 unfolding closed_int_def by auto

346 with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"

347 unfolding closed_int_def by auto

348 with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"

349 by simp

350 then show ?thesis by auto

351 qed

353 subsection {* newInt: Interval generation *}

355 text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a

356 closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and

357 does not contain @{text "f (Suc n)"}. With the base case defined such

358 that @{text "(f 0)\<notin>newInt 0 f"}. *}

360 subsubsection {* Definition *}

362 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where

363 "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"

364 | "newInt (Suc n) f =

365 (SOME e. (\<exists>e1 e2.

366 e1 < e2 \<and>

367 e = closed_int e1 e2 \<and>

368 e \<subseteq> (newInt n f) \<and>

369 (f (Suc n)) \<notin> e)

370 )"

373 subsubsection {* Properties *}

375 text {* We now show that every application of newInt returns an

376 appropriate interval. *}

378 lemma newInt_ex:

379 "\<exists>a b. a < b \<and>

380 newInt (Suc n) f = closed_int a b \<and>

381 newInt (Suc n) f \<subseteq> newInt n f \<and>

382 f (Suc n) \<notin> newInt (Suc n) f"

383 proof (induct n)

384 case 0

386 let ?e = "SOME e. \<exists>e1 e2.

387 e1 < e2 \<and>

388 e = closed_int e1 e2 \<and>

389 e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

390 f (Suc 0) \<notin> e"

392 have "newInt (Suc 0) f = ?e" by auto

393 moreover

394 have "f 0 + 1 < f 0 + 2" by simp

395 with closed_subset_ex have

396 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

397 f (Suc 0) \<notin> (closed_int ka kb)" .

398 hence

399 "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

400 e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp

401 hence

402 "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>

403 ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"

404 by (rule someI_ex)

405 ultimately have "\<exists>e1 e2. e1 < e2 \<and>

406 newInt (Suc 0) f = closed_int e1 e2 \<and>

407 newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

408 f (Suc 0) \<notin> newInt (Suc 0) f" by simp

409 thus

410 "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>

411 newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"

412 by simp

413 next

414 case (Suc n)

415 hence "\<exists>a b.

416 a < b \<and>

417 newInt (Suc n) f = closed_int a b \<and>

418 newInt (Suc n) f \<subseteq> newInt n f \<and>

419 f (Suc n) \<notin> newInt (Suc n) f" by simp

420 then obtain a and b where ab: "a < b \<and>

421 newInt (Suc n) f = closed_int a b \<and>

422 newInt (Suc n) f \<subseteq> newInt n f \<and>

423 f (Suc n) \<notin> newInt (Suc n) f" by auto

424 hence cab: "closed_int a b = newInt (Suc n) f" by simp

426 let ?e = "SOME e. \<exists>e1 e2.

427 e1 < e2 \<and>

428 e = closed_int e1 e2 \<and>

429 e \<subseteq> closed_int a b \<and>

430 f (Suc (Suc n)) \<notin> e"

431 from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto

433 from ab have "a < b" by simp

434 with closed_subset_ex have

435 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>

436 f (Suc (Suc n)) \<notin> closed_int ka kb" .

437 hence

438 "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

439 closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"

440 by simp

441 hence

442 "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

443 e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp

444 hence

445 "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>

446 ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)

447 with ab ni show

448 "\<exists>ka kb. ka < kb \<and>

449 newInt (Suc (Suc n)) f = closed_int ka kb \<and>

450 newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>

451 f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto

452 qed

454 lemma newInt_subset:

455 "newInt (Suc n) f \<subseteq> newInt n f"

456 using newInt_ex by auto

459 text {* Another fundamental property is that no element in the range

460 of f is in the intersection of all closed intervals generated by

461 newInt. *}

463 lemma newInt_inter:

464 "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"

465 proof

466 fix n::nat

467 {

468 assume n0: "n = 0"

469 moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp

470 ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)

471 }

472 moreover

473 {

474 assume "\<not> n = 0"

475 hence "n > 0" by simp

476 then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)

478 from newInt_ex have

479 "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>

480 newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .

481 then have "f (Suc m) \<notin> newInt (Suc m) f" by auto

482 with ndef have "f n \<notin> newInt n f" by simp

483 }

484 ultimately have "f n \<notin> newInt n f" by (rule case_split)

485 thus "f n \<notin> (\<Inter>n. newInt n f)" by auto

486 qed

489 lemma newInt_notempty:

490 "(\<Inter>n. newInt n f) \<noteq> {}"

491 proof -

492 let ?g = "\<lambda>n. newInt n f"

493 have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"

494 proof

495 fix n

496 show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)

497 qed

498 moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"

499 proof

500 fix n::nat

501 {

502 assume "n = 0"

503 then have

504 "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"

505 by simp

506 hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast

507 }

508 moreover

509 {

510 assume "\<not> n = 0"

511 then have "n > 0" by simp

512 then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)

514 have

515 "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>

516 (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"

517 by (rule newInt_ex)

518 then obtain a and b where

519 "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto

520 with nd have "?g n = closed_int a b \<and> a \<le> b" by auto

521 hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast

522 }

523 ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)

524 qed

525 ultimately show ?thesis by (rule NIP)

526 qed

529 subsection {* Final Theorem *}

531 theorem real_non_denum:

532 shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"

533 proof -- "by contradiction"

534 assume "\<exists>f::nat\<Rightarrow>real. surj f"

535 then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto

536 -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "

537 have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast

538 moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)

539 ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast

540 moreover from rangeF have "x \<in> range f" by simp

541 ultimately show False by blast

542 qed

544 end