author  hoelzl 
Wed, 18 Dec 2013 11:53:40 +0100  
changeset 54797  be020ec8560c 
parent 54263  c4159fe6fa46 
child 56796  9f84219715a7 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

1 
(* Title : HOL/ContNonDenum 
23461  2 
Author : Benjamin Porter, Monash University, NICTA, 2005 
3 
*) 

4 

5 
header {* Nondenumerability of the Continuum. *} 

6 

7 
theory ContNotDenum 

30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
29026
diff
changeset

8 
imports Complex_Main 
23461  9 
begin 
10 

11 
subsection {* Abstract *} 

12 

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. 

16 

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. 

20 

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 nonempty. 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. *} 

31 

32 
subsection {* Closed Intervals *} 

33 

34 
subsection {* Nested Interval Property *} 

35 

36 
theorem NIP: 

37 
fixes f::"nat \<Rightarrow> real set" 

38 
assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n" 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

39 
and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b" 
23461  40 
shows "(\<Inter>n. f n) \<noteq> {}" 
41 
proof  

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

42 
let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

43 
{ fix n 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

44 
from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

45 
by auto 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

46 
then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

47 
by auto } 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

48 
note f_eq = this 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

49 
{ fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

50 
by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) } 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

51 
note subset' = this 
23461  52 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

53 
have "compact (f 0)" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

54 
by (subst f_eq) (rule compact_Icc) 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

55 
then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

56 
proof (rule compact_imp_fip_image) 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

57 
fix I :: "nat set" assume I: "finite I" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

58 
have "{} \<subset> f (Max (insert 0 I))" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

59 
using f_eq[of "Max (insert 0 I)"] by auto 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

60 
also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

61 
proof (rule INF_greatest) 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

62 
fix i assume "i \<in> insert 0 I" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

63 
with I show "f (Max (insert 0 I)) \<subseteq> f i" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

64 
by (intro subset') auto 
23461  65 
qed 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

66 
finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

67 
by auto 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

68 
qed (subst f_eq, auto) 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

69 
then show "(\<Inter>n. f n) \<noteq> {}" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

70 
by auto 
23461  71 
qed 
72 

73 
subsection {* Generating the intervals *} 

74 

75 
subsubsection {* Existence of nonsingleton closed intervals *} 

76 

77 
text {* This lemma asserts that given any nonsingleton closed 

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

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

80 
nonsingleton itself. *} 

81 

82 
lemma closed_subset_ex: 

83 
fixes c::real 

53372  84 
assumes "a < b" 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

85 
shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}" 
53372  86 
proof (cases "c < b") 
87 
case True 

88 
show ?thesis 

89 
proof (cases "c < a") 

90 
case True 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

91 
with `a < b` `c < b` have "c \<notin> {a..b}" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

92 
by auto 
53372  93 
with `a < b` show ?thesis by auto 
94 
next 

95 
case False 

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

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

23461  98 

53372  99 
from ka_def `c < b` have kalb: "ka < b" by auto 
100 
moreover from ka_def `c < b` have kagc: "ka > c" by simp 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

101 
ultimately have "c\<notin>{ka..b}" by auto 
53372  102 
moreover from `a \<le> c` kagc have "ka \<ge> a" by simp 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

103 
hence "{ka..b} \<subseteq> {a..b}" by auto 
23461  104 
ultimately have 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

105 
"ka < b \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}" 
53372  106 
using kalb by auto 
107 
then show ?thesis 

108 
by auto 

109 
qed 

110 
next 

111 
case False 

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

23461  113 

53372  114 
def kb \<equiv> "(a + b)/2" 
115 
with `a < b` have "kb < b" by auto 

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

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

117 
from `kb < c` have c: "c \<notin> {a..kb}" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

118 
by auto 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

119 
with `kb < b` have "{a..kb} \<subseteq> {a..b}" 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

120 
by auto 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

121 
with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}" 
53372  122 
by simp 
123 
then show ?thesis by auto 

23461  124 
qed 
125 

126 
subsection {* newInt: Interval generation *} 

127 

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

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

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

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

132 

133 
subsubsection {* Definition *} 

134 

27435  135 
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

136 
"newInt 0 f = {f 0 + 1..f 0 + 2}" 
27435  137 
 "newInt (Suc n) f = 
138 
(SOME e. (\<exists>e1 e2. 

139 
e1 < e2 \<and> 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

140 
e = {e1..e2} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

141 
e \<subseteq> newInt n f \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

142 
f (Suc n) \<notin> e) 
27435  143 
)" 
144 

23461  145 

146 
subsubsection {* Properties *} 

147 

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

149 
appropriate interval. *} 

150 

151 
lemma newInt_ex: 

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

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

153 
newInt (Suc n) f = {a..b} \<and> 
23461  154 
newInt (Suc n) f \<subseteq> newInt n f \<and> 
155 
f (Suc n) \<notin> newInt (Suc n) f" 

156 
proof (induct n) 

157 
case 0 

158 

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

160 
e1 < e2 \<and> 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

161 
e = {e1..e2} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

162 
e \<subseteq> {f 0 + 1..f 0 + 2} \<and> 
23461  163 
f (Suc 0) \<notin> e" 
164 

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

166 
moreover 

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

168 
with closed_subset_ex have 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

169 
"\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

170 
f (Suc 0) \<notin> {ka..kb}" . 
23461  171 
hence 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

172 
"\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

173 
e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp 
23461  174 
hence 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

175 
"\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e" 
23461  176 
by (rule someI_ex) 
177 
ultimately have "\<exists>e1 e2. e1 < e2 \<and> 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

178 
newInt (Suc 0) f = {e1..e2} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

179 
newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and> 
23461  180 
f (Suc 0) \<notin> newInt (Suc 0) f" by simp 
181 
thus 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

182 
"\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and> 
23461  183 
newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f" 
184 
by simp 

185 
next 

186 
case (Suc n) 

187 
hence "\<exists>a b. 

188 
a < b \<and> 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

189 
newInt (Suc n) f = {a..b} \<and> 
23461  190 
newInt (Suc n) f \<subseteq> newInt n f \<and> 
191 
f (Suc n) \<notin> newInt (Suc n) f" by simp 

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

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

193 
newInt (Suc n) f = {a..b} \<and> 
23461  194 
newInt (Suc n) f \<subseteq> newInt n f \<and> 
195 
f (Suc n) \<notin> newInt (Suc n) f" by auto 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

196 
hence cab: "{a..b} = newInt (Suc n) f" by simp 
23461  197 

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

199 
e1 < e2 \<and> 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

200 
e = {e1..e2} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

201 
e \<subseteq> {a..b} \<and> 
23461  202 
f (Suc (Suc n)) \<notin> e" 
203 
from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto 

204 

205 
from ab have "a < b" by simp 

206 
with closed_subset_ex have 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

207 
"\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

208 
f (Suc (Suc n)) \<notin> {ka..kb}" . 
23461  209 
hence 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

210 
"\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

211 
{ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}" 
23461  212 
by simp 
213 
hence 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

214 
"\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

215 
e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp 
23461  216 
hence 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

217 
"\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

218 
?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex) 
23461  219 
with ab ni show 
220 
"\<exists>ka kb. ka < kb \<and> 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

221 
newInt (Suc (Suc n)) f = {ka..kb} \<and> 
23461  222 
newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and> 
223 
f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto 

224 
qed 

225 

226 
lemma newInt_subset: 

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

228 
using newInt_ex by auto 

229 

230 

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

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

233 
newInt. *} 

234 

235 
lemma newInt_inter: 

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

237 
proof 

238 
fix n::nat 

239 
{ 

240 
assume n0: "n = 0" 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

241 
moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

242 
ultimately have "f n \<notin> newInt n f" by simp 
23461  243 
} 
244 
moreover 

245 
{ 

246 
assume "\<not> n = 0" 

247 
hence "n > 0" by simp 

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

249 

250 
from newInt_ex have 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

251 
"\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and> 
23461  252 
newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" . 
253 
then have "f (Suc m) \<notin> newInt (Suc m) f" by auto 

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

255 
} 

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

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

258 
qed 

259 

260 

261 
lemma newInt_notempty: 

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

263 
proof  

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

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

266 
proof 

267 
fix n 

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

269 
qed 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

270 
moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b" 
23461  271 
proof 
272 
fix n::nat 

273 
{ 

274 
assume "n = 0" 

275 
then have 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

276 
"?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)" 
23461  277 
by simp 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

278 
hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast 
23461  279 
} 
280 
moreover 

281 
{ 

282 
assume "\<not> n = 0" 

283 
then have "n > 0" by simp 

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

285 

286 
have 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

287 
"\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and> 
23461  288 
(newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)" 
289 
by (rule newInt_ex) 

290 
then obtain a and b where 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

291 
"a < b \<and> (newInt (Suc m) f) = {a..b}" by auto 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

292 
with nd have "?g n = {a..b} \<and> a \<le> b" by auto 
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

293 
hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast 
23461  294 
} 
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

295 
ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split) 
23461  296 
qed 
297 
ultimately show ?thesis by (rule NIP) 

298 
qed 

299 

300 

301 
subsection {* Final Theorem *} 

302 

303 
theorem real_non_denum: 

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

305 
proof  "by contradiction" 

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

40702  307 
then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto 
23461  308 
 "We now produce a real number x that is not in the range of f, using the properties of newInt. " 
309 
have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast 

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

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

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

313 
ultimately show False by blast 

314 
qed 

315 

316 
end 

54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset

317 