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

src/HOL/Library/ContNotDenum.thy

author | haftmann |

Fri Aug 27 19:34:23 2010 +0200 (2010-08-27 ago) | |

changeset 38857 | 97775f3e8722 |

parent 37765 | 26bdfb7b680b |

child 40702 | cf26dd7395e4 |

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

renamed class/constant eq to equal; tuned some instantiations

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 "surj f" by auto

569 hence rangeF: "range f = UNIV" by (rule surj_range)

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

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

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

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

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

575 ultimately show False by blast

576 qed

578 end