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

src/HOL/Library/ContNotDenum.thy

author | haftmann |

Fri Nov 01 18:51:14 2013 +0100 (2013-11-01) | |

changeset 54230 | b1d955791529 |

parent 53372 | f5a6313c7fe4 |

child 54263 | c4159fe6fa46 |

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

more simplification rules on unary and binary minus

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 "a < b"

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

328 proof (cases "c < b")

329 case True

330 show ?thesis

331 proof (cases "c < a")

332 case True

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

334 unfolding closed_int_def by auto

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

336 next

337 case False

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

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

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

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

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

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

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

346 ultimately have

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

348 using kalb by auto

349 then show ?thesis

350 by auto

351 qed

352 next

353 case False

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

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

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

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

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

360 unfolding closed_int_def by auto

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

362 unfolding closed_int_def by auto

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

364 by simp

365 then show ?thesis by auto

366 qed

368 subsection {* newInt: Interval generation *}

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

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

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

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

375 subsubsection {* Definition *}

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

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

379 | "newInt (Suc n) f =

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

381 e1 < e2 \<and>

382 e = closed_int e1 e2 \<and>

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

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

385 )"

388 subsubsection {* Properties *}

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

391 appropriate interval. *}

393 lemma newInt_ex:

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

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

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

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

398 proof (induct n)

399 case 0

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

402 e1 < e2 \<and>

403 e = closed_int e1 e2 \<and>

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

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

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

408 moreover

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

410 with closed_subset_ex have

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

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

413 hence

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

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

416 hence

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

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

419 by (rule someI_ex)

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

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

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

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

424 thus

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

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

427 by simp

428 next

429 case (Suc n)

430 hence "\<exists>a b.

431 a < b \<and>

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

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

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

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

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

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

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

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

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

442 e1 < e2 \<and>

443 e = closed_int e1 e2 \<and>

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

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

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

448 from ab have "a < b" by simp

449 with closed_subset_ex have

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

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

452 hence

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

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

455 by simp

456 hence

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

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

459 hence

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

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

462 with ab ni show

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

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

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

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

467 qed

469 lemma newInt_subset:

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

471 using newInt_ex by auto

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

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

476 newInt. *}

478 lemma newInt_inter:

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

480 proof

481 fix n::nat

482 {

483 assume n0: "n = 0"

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

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

486 }

487 moreover

488 {

489 assume "\<not> n = 0"

490 hence "n > 0" by simp

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

493 from newInt_ex have

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

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

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

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

498 }

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

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

501 qed

504 lemma newInt_notempty:

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

506 proof -

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

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

509 proof

510 fix n

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

512 qed

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

514 proof

515 fix n::nat

516 {

517 assume "n = 0"

518 then have

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

520 by simp

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

522 }

523 moreover

524 {

525 assume "\<not> n = 0"

526 then have "n > 0" by simp

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

529 have

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

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

532 by (rule newInt_ex)

533 then obtain a and b where

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

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

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

537 }

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

539 qed

540 ultimately show ?thesis by (rule NIP)

541 qed

544 subsection {* Final Theorem *}

546 theorem real_non_denum:

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

548 proof -- "by contradiction"

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

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

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

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

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

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

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

556 ultimately show False by blast

557 qed

559 end