129 thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex) |
129 thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex) |
130 qed |
130 qed |
131 |
131 |
132 -- "A denotes the set of all left-most points of all the intervals ..." |
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 |
133 moreover obtain A where Adef: "A = ?g ` \<nat>" by simp |
134 ultimately have "\<exists>x. x\<in>A" |
134 ultimately have "A \<noteq> {}" |
135 proof - |
135 proof - |
136 have "(0::nat) \<in> \<nat>" by simp |
136 have "(0::nat) \<in> \<nat>" by simp |
137 moreover have "?g 0 = ?g 0" by simp |
137 with Adef show ?thesis |
138 ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule rev_image_eqI) |
138 by blast |
139 with Adef have "?g 0 \<in> A" by simp |
|
140 thus ?thesis .. |
|
141 qed |
139 qed |
142 |
140 |
143 -- "Now show that A is bounded above ..." |
141 -- "Now show that A is bounded above ..." |
144 moreover have "\<exists>y. isUb (UNIV::real set) A y" |
142 moreover have "bdd_above A" |
145 proof - |
143 proof - |
146 { |
144 { |
147 fix n |
145 fix n |
148 from ne have ex: "\<exists>x. x\<in>(f n)" .. |
146 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 |
147 from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp |
175 qed |
173 qed |
176 moreover from closed |
174 moreover from closed |
177 obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast |
175 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 |
176 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 |
177 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 |
178 with Adef show "bdd_above A" by auto |
181 hence "A *<= b" by (unfold setle_def) |
179 qed |
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) |
|
189 |
180 |
190 -- "denote this least upper bound as t ..." |
181 -- "denote this least upper bound as t ..." |
191 then obtain t where tdef: "isLub UNIV A t" .. |
182 def tdef: t == "Sup A" |
192 |
183 |
193 -- "and finally show that this least upper bound is in all the intervals..." |
184 -- "and finally show that this least upper bound is in all the intervals..." |
194 have "\<forall>n. t \<in> f n" |
185 have "\<forall>n. t \<in> f n" |
195 proof |
186 proof |
196 fix n::nat |
187 fix n::nat |
227 . |
218 . |
228 } |
219 } |
229 with Adef have "(?g n) \<in> A" by auto |
220 with Adef have "(?g n) \<in> A" by auto |
230 ultimately show ?thesis by simp |
221 ultimately show ?thesis by simp |
231 qed |
222 qed |
232 with tdef show "a \<le> t" by (rule isLubD2) |
223 with `bdd_above A` show "a \<le> t" |
|
224 unfolding tdef by (intro cSup_upper) |
233 qed |
225 qed |
234 moreover have "t \<le> b" |
226 moreover have "t \<le> b" |
235 proof - |
227 unfolding tdef |
236 have "isUb UNIV A b" |
228 proof (rule cSup_least) |
237 proof - |
229 { |
|
230 from alb int have |
|
231 ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast |
|
232 |
|
233 have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n" |
|
234 proof (rule allI, induct_tac m) |
|
235 show "\<forall>n. f (n + 0) \<subseteq> f n" by simp |
|
236 next |
|
237 fix m n |
|
238 assume pp: "\<forall>p. f (p + n) \<subseteq> f p" |
|
239 { |
|
240 fix p |
|
241 from pp have "f (p + n) \<subseteq> f p" by simp |
|
242 moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto |
|
243 hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp |
|
244 ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp |
|
245 } |
|
246 thus "\<forall>p. f (p + Suc n) \<subseteq> f p" .. |
|
247 qed |
|
248 have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)" |
|
249 proof ((rule allI)+, rule impI) |
|
250 fix \<alpha>::nat and \<beta>::nat |
|
251 assume "\<beta> \<le> \<alpha>" |
|
252 hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add) |
|
253 then obtain k where "\<alpha> = \<beta> + k" .. |
|
254 moreover |
|
255 from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp |
|
256 ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto |
|
257 qed |
|
258 |
|
259 fix m |
238 { |
260 { |
239 from alb int have |
261 assume "m \<ge> n" |
240 ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast |
262 with subsetm have "f m \<subseteq> f n" by simp |
241 |
263 with ain have "\<forall>x\<in>f m. x \<le> b" by auto |
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 |
|
267 |
|
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 |
264 moreover |
278 { |
265 from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp |
279 assume "\<not>(m \<ge> n)" |
266 ultimately have "?g m \<le> b" by auto |
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 } |
267 } |
300 with Adef have "\<forall>y\<in>A. y\<le>b" by auto |
268 moreover |
301 hence "A *<= b" by (unfold setle_def) |
269 { |
302 moreover have "b \<in> (UNIV::real set)" by simp |
270 assume "\<not>(m \<ge> n)" |
303 ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp |
271 hence "m < n" by simp |
304 thus "isUb (UNIV::real set) A b" by (unfold isUb_def) |
272 with subsetm have sub: "(f n) \<subseteq> (f m)" by simp |
305 qed |
273 from closed obtain ma and mb where |
306 with tdef show "t \<le> b" by (rule isLub_le_isUb) |
274 "f m = closed_int ma mb \<and> ma \<le> mb" by blast |
307 qed |
275 hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto |
|
276 from one alb sub fm int have "ma \<le> b" using closed_subset by blast |
|
277 moreover have "(?g m) = ma" |
|
278 proof - |
|
279 from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" .. |
|
280 moreover from one have |
|
281 "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)" |
|
282 by (rule closed_int_least) |
|
283 with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp |
|
284 ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto |
|
285 thus "?g m = ma" by auto |
|
286 qed |
|
287 ultimately have "?g m \<le> b" by simp |
|
288 } |
|
289 ultimately have "?g m \<le> b" by (rule case_split) |
|
290 } |
|
291 with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto |
|
292 qed fact |
308 ultimately have "t \<in> closed_int a b" by (rule closed_mem) |
293 ultimately have "t \<in> closed_int a b" by (rule closed_mem) |
309 with int show "t \<in> f n" by simp |
294 with int show "t \<in> f n" by simp |
310 qed |
295 qed |
311 hence "t \<in> (\<Inter>n. f n)" by auto |
296 hence "t \<in> (\<Inter>n. f n)" by auto |
312 thus ?thesis by auto |
297 thus ?thesis by auto |