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

src/HOL/Library/ContNotDenum.thy

author | haftmann |

Wed Apr 22 19:09:21 2009 +0200 (2009-04-22) | |

changeset 30960 | fec1a04b7220 |

parent 30663 | 0b6aff7451b2 |

child 37765 | 26bdfb7b680b |

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

power operation defined generic

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 )"

405 declare newInt.simps [code del]

407 subsubsection {* Properties *}

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

410 appropriate interval. *}

412 lemma newInt_ex:

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

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

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

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

417 proof (induct n)

418 case 0

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

421 e1 < e2 \<and>

422 e = closed_int e1 e2 \<and>

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

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

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

427 moreover

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

429 with closed_subset_ex have

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

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

432 hence

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

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

435 hence

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

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

438 by (rule someI_ex)

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

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

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

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

443 thus

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

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

446 by simp

447 next

448 case (Suc n)

449 hence "\<exists>a b.

450 a < b \<and>

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

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

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

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

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

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

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

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

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

461 e1 < e2 \<and>

462 e = closed_int e1 e2 \<and>

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

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

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

467 from ab have "a < b" by simp

468 with closed_subset_ex have

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

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

471 hence

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

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

474 by simp

475 hence

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

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

478 hence

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

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

481 with ab ni show

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

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

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

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

486 qed

488 lemma newInt_subset:

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

490 using newInt_ex by auto

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

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

495 newInt. *}

497 lemma newInt_inter:

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

499 proof

500 fix n::nat

501 {

502 assume n0: "n = 0"

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

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

505 }

506 moreover

507 {

508 assume "\<not> n = 0"

509 hence "n > 0" by simp

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

512 from newInt_ex have

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

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

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

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

517 }

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

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

520 qed

523 lemma newInt_notempty:

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

525 proof -

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

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

528 proof

529 fix n

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

531 qed

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

533 proof

534 fix n::nat

535 {

536 assume "n = 0"

537 then have

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

539 by simp

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

541 }

542 moreover

543 {

544 assume "\<not> n = 0"

545 then have "n > 0" by simp

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

548 have

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

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

551 by (rule newInt_ex)

552 then obtain a and b where

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

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

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

556 }

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

558 qed

559 ultimately show ?thesis by (rule NIP)

560 qed

563 subsection {* Final Theorem *}

565 theorem real_non_denum:

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

567 proof -- "by contradiction"

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

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

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

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

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

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

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

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

576 ultimately show False by blast

577 qed

579 end