10751
|
1 |
(* Title : SEQ.thy
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
4 |
Description : Convergence of sequences and series
|
15082
|
5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
|
|
6 |
*)
|
10751
|
7 |
|
15082
|
8 |
theory SEQ = NatStar + HyperPow:
|
10751
|
9 |
|
|
10 |
constdefs
|
|
11 |
|
15082
|
12 |
LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60)
|
|
13 |
--{*Standard definition of convergence of sequence*}
|
|
14 |
"X ----> L == (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
|
10751
|
15 |
|
15082
|
16 |
NSLIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----NS> (_))" [60, 60] 60)
|
|
17 |
--{*Nonstandard definition of convergence of sequence*}
|
|
18 |
"X ----NS> L == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)"
|
|
19 |
|
|
20 |
lim :: "(nat => real) => real"
|
|
21 |
--{*Standard definition of limit using choice operator*}
|
10751
|
22 |
"lim X == (@L. (X ----> L))"
|
|
23 |
|
15082
|
24 |
nslim :: "(nat => real) => real"
|
|
25 |
--{*Nonstandard definition of limit using choice operator*}
|
10751
|
26 |
"nslim X == (@L. (X ----NS> L))"
|
|
27 |
|
15082
|
28 |
convergent :: "(nat => real) => bool"
|
|
29 |
--{*Standard definition of convergence*}
|
|
30 |
"convergent X == (\<exists>L. (X ----> L))"
|
10751
|
31 |
|
15082
|
32 |
NSconvergent :: "(nat => real) => bool"
|
|
33 |
--{*Nonstandard definition of convergence*}
|
|
34 |
"NSconvergent X == (\<exists>L. (X ----NS> L))"
|
|
35 |
|
|
36 |
Bseq :: "(nat => real) => bool"
|
|
37 |
--{*Standard definition for bounded sequence*}
|
|
38 |
"Bseq X == (\<exists>K. (0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)))"
|
10751
|
39 |
|
15082
|
40 |
NSBseq :: "(nat=>real) => bool"
|
|
41 |
--{*Nonstandard definition for bounded sequence*}
|
|
42 |
"NSBseq X == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite)"
|
|
43 |
|
|
44 |
monoseq :: "(nat=>real)=>bool"
|
|
45 |
--{*Definition for monotonicity*}
|
|
46 |
"monoseq X == ((\<forall>(m::nat) n. m \<le> n --> X m \<le> X n) |
|
|
47 |
(\<forall>m n. m \<le> n --> X n \<le> X m))"
|
10751
|
48 |
|
15082
|
49 |
subseq :: "(nat => nat) => bool"
|
|
50 |
--{*Definition of subsequence*}
|
|
51 |
"subseq f == (\<forall>m n. m < n --> (f m) < (f n))"
|
10751
|
52 |
|
15082
|
53 |
Cauchy :: "(nat => real) => bool"
|
|
54 |
--{*Standard definition of the Cauchy condition*}
|
|
55 |
"Cauchy X == (\<forall>e. (0 < e -->
|
|
56 |
(\<exists>M. (\<forall>m n. M \<le> m & M \<le> n
|
10751
|
57 |
--> abs((X m) + -(X n)) < e))))"
|
|
58 |
|
15082
|
59 |
NSCauchy :: "(nat => real) => bool"
|
|
60 |
--{*Nonstandard definition*}
|
|
61 |
"NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite.
|
|
62 |
( *fNat* X) M \<approx> ( *fNat* X) N)"
|
|
63 |
|
|
64 |
|
|
65 |
|
|
66 |
text{* Example of an hypersequence (i.e. an extended standard sequence)
|
|
67 |
whose term with an hypernatural suffix is an infinitesimal i.e.
|
|
68 |
the whn'nth term of the hypersequence is a member of Infinitesimal*}
|
|
69 |
|
|
70 |
lemma SEQ_Infinitesimal:
|
|
71 |
"( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
|
|
72 |
apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
|
|
73 |
apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
|
|
74 |
apply (simp add: real_of_nat_Suc_gt_zero abs_eqI2 FreeUltrafilterNat_inverse_real_of_posnat)
|
|
75 |
done
|
|
76 |
|
|
77 |
|
|
78 |
subsection{*LIMSEQ and NSLIMSEQ*}
|
|
79 |
|
|
80 |
lemma LIMSEQ_iff:
|
|
81 |
"(X ----> L) =
|
|
82 |
(\<forall>r. 0 <r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
|
|
83 |
by (simp add: LIMSEQ_def)
|
|
84 |
|
|
85 |
lemma NSLIMSEQ_iff:
|
|
86 |
"(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)"
|
|
87 |
by (simp add: NSLIMSEQ_def)
|
|
88 |
|
|
89 |
|
|
90 |
text{*LIMSEQ ==> NSLIMSEQ*}
|
|
91 |
|
|
92 |
lemma LIMSEQ_NSLIMSEQ:
|
|
93 |
"X ----> L ==> X ----NS> L"
|
|
94 |
apply (simp add: LIMSEQ_def NSLIMSEQ_def)
|
|
95 |
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
|
|
96 |
apply (rule_tac z = N in eq_Abs_hypnat)
|
|
97 |
apply (rule approx_minus_iff [THEN iffD2])
|
|
98 |
apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def
|
|
99 |
hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
|
|
100 |
apply (rule bexI [OF _ lemma_hyprel_refl], safe)
|
|
101 |
apply (drule_tac x = u in spec, safe)
|
|
102 |
apply (drule_tac x = no in spec, fuf)
|
|
103 |
apply (blast dest: less_imp_le)
|
|
104 |
done
|
|
105 |
|
|
106 |
|
|
107 |
text{*NSLIMSEQ ==> LIMSEQ*}
|
|
108 |
|
|
109 |
lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). \<forall>n. n \<le> f n
|
|
110 |
==> {n. f n = 0} = {0} | {n. f n = 0} = {}"
|
|
111 |
apply auto
|
|
112 |
apply (drule_tac x = xa in spec)
|
|
113 |
apply (drule_tac [2] x = x in spec, auto)
|
|
114 |
done
|
|
115 |
|
|
116 |
lemma lemma_NSLIMSEQ2: "{n. f n \<le> Suc u} = {n. f n \<le> u} Un {n. f n = Suc u}"
|
|
117 |
by (auto simp add: le_Suc_eq)
|
|
118 |
|
|
119 |
lemma lemma_NSLIMSEQ3:
|
|
120 |
"!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. f n = Suc u} \<le> {n. n \<le> Suc u}"
|
|
121 |
apply auto
|
|
122 |
apply (drule_tac x = x in spec, auto)
|
|
123 |
done
|
|
124 |
|
|
125 |
text{* the following sequence @{term "f(n)"} defines a hypernatural *}
|
|
126 |
lemma NSLIMSEQ_finite_set:
|
|
127 |
"!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
|
|
128 |
apply (induct u)
|
|
129 |
apply (auto simp add: lemma_NSLIMSEQ2)
|
|
130 |
apply (auto intro: lemma_NSLIMSEQ3 [THEN finite_subset] finite_atMost [unfolded atMost_def])
|
|
131 |
apply (drule lemma_NSLIMSEQ1, safe)
|
|
132 |
apply (simp_all (no_asm_simp))
|
|
133 |
done
|
|
134 |
|
|
135 |
lemma Compl_less_set: "- {n. u < (f::nat=>nat) n} = {n. f n \<le> u}"
|
|
136 |
by (auto dest: less_le_trans simp add: le_def)
|
|
137 |
|
|
138 |
text{* the index set is in the free ultrafilter *}
|
|
139 |
lemma FreeUltrafilterNat_NSLIMSEQ:
|
|
140 |
"!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. u < f n} : FreeUltrafilterNat"
|
|
141 |
apply (rule FreeUltrafilterNat_Compl_iff2 [THEN iffD2])
|
|
142 |
apply (rule FreeUltrafilterNat_finite)
|
|
143 |
apply (auto dest: NSLIMSEQ_finite_set simp add: Compl_less_set)
|
|
144 |
done
|
|
145 |
|
|
146 |
text{* thus, the sequence defines an infinite hypernatural! *}
|
|
147 |
lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
|
|
148 |
==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite"
|
|
149 |
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
|
|
150 |
apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
|
|
151 |
apply (erule FreeUltrafilterNat_NSLIMSEQ)
|
|
152 |
done
|
|
153 |
|
|
154 |
lemma lemmaLIM:
|
|
155 |
"{n. X (f n) + - L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le>
|
|
156 |
{n. \<bar>X (f n) + - L\<bar> < r}"
|
|
157 |
by auto
|
|
158 |
|
|
159 |
lemma lemmaLIM2:
|
|
160 |
"{n. \<bar>X (f n) + - L\<bar> < r} Int {n. r \<le> abs (X (f n) + - (L::real))} = {}"
|
|
161 |
by auto
|
|
162 |
|
|
163 |
lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
|
|
164 |
( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) +
|
|
165 |
- hypreal_of_real L \<approx> 0 |] ==> False"
|
|
166 |
apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
|
|
167 |
apply (rename_tac "Y")
|
|
168 |
apply (drule_tac x = r in spec, safe)
|
|
169 |
apply (drule FreeUltrafilterNat_Int, assumption)
|
|
170 |
apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
|
|
171 |
apply (drule FreeUltrafilterNat_all)
|
|
172 |
apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
|
|
173 |
apply (drule FreeUltrafilterNat_Int, assumption)
|
|
174 |
apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty)
|
|
175 |
done
|
|
176 |
|
|
177 |
lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L"
|
|
178 |
apply (simp add: LIMSEQ_def NSLIMSEQ_def)
|
|
179 |
apply (rule ccontr, simp, safe)
|
|
180 |
txt{* skolemization step *}
|
|
181 |
apply (drule choice, safe)
|
|
182 |
apply (drule_tac x = "Abs_hypnat (hypnatrel``{f}) " in bspec)
|
|
183 |
apply (drule_tac [2] approx_minus_iff [THEN iffD1])
|
|
184 |
apply (simp_all add: linorder_not_less)
|
|
185 |
apply (blast intro: HNatInfinite_NSLIMSEQ)
|
|
186 |
apply (blast intro: lemmaLIM3)
|
|
187 |
done
|
|
188 |
|
|
189 |
text{* Now, the all-important result is trivially proved! *}
|
|
190 |
theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
|
|
191 |
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
|
|
192 |
|
|
193 |
|
|
194 |
subsection{*Theorems About Sequences*}
|
|
195 |
|
|
196 |
lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
|
|
197 |
by (simp add: NSLIMSEQ_def)
|
|
198 |
|
|
199 |
lemma LIMSEQ_const: "(%n. k) ----> k"
|
|
200 |
by (simp add: LIMSEQ_def)
|
|
201 |
|
|
202 |
lemma NSLIMSEQ_add:
|
|
203 |
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
|
|
204 |
by (auto intro: approx_add simp add: NSLIMSEQ_def starfunNat_add [symmetric])
|
|
205 |
|
|
206 |
lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
|
|
207 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
|
|
208 |
|
|
209 |
lemma NSLIMSEQ_mult:
|
|
210 |
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
|
|
211 |
by (auto intro!: approx_mult_HFinite
|
|
212 |
simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric])
|
|
213 |
|
|
214 |
lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
|
|
215 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
|
|
216 |
|
|
217 |
lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
|
|
218 |
by (auto simp add: NSLIMSEQ_def starfunNat_minus [symmetric])
|
|
219 |
|
|
220 |
lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a"
|
|
221 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus)
|
|
222 |
|
|
223 |
lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a"
|
|
224 |
by (drule LIMSEQ_minus, simp)
|
|
225 |
|
|
226 |
lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
|
|
227 |
by (drule NSLIMSEQ_minus, simp)
|
|
228 |
|
|
229 |
lemma NSLIMSEQ_add_minus:
|
|
230 |
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
|
|
231 |
by (simp add: NSLIMSEQ_add NSLIMSEQ_minus [of Y])
|
|
232 |
|
|
233 |
lemma LIMSEQ_add_minus:
|
|
234 |
"[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
|
|
235 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus)
|
|
236 |
|
|
237 |
lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b"
|
|
238 |
apply (simp add: diff_minus)
|
|
239 |
apply (blast intro: LIMSEQ_add_minus)
|
|
240 |
done
|
|
241 |
|
|
242 |
lemma NSLIMSEQ_diff:
|
|
243 |
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
|
|
244 |
apply (simp add: diff_minus)
|
|
245 |
apply (blast intro: NSLIMSEQ_add_minus)
|
|
246 |
done
|
|
247 |
|
|
248 |
text{*Proof is like that of @{text NSLIM_inverse}.*}
|
|
249 |
lemma NSLIMSEQ_inverse:
|
|
250 |
"[| X ----NS> a; a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
|
|
251 |
by (simp add: NSLIMSEQ_def starfunNat_inverse [symmetric]
|
|
252 |
hypreal_of_real_approx_inverse)
|
|
253 |
|
|
254 |
|
|
255 |
text{*Standard version of theorem*}
|
|
256 |
lemma LIMSEQ_inverse:
|
|
257 |
"[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
|
|
258 |
by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
|
|
259 |
|
|
260 |
lemma NSLIMSEQ_mult_inverse:
|
|
261 |
"[| X ----NS> a; Y ----NS> b; b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
|
|
262 |
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
|
|
263 |
|
|
264 |
lemma LIMSEQ_divide:
|
|
265 |
"[| X ----> a; Y ----> b; b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
|
|
266 |
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
|
|
267 |
|
|
268 |
text{*Uniqueness of limit*}
|
|
269 |
lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
|
|
270 |
apply (simp add: NSLIMSEQ_def)
|
|
271 |
apply (drule HNatInfinite_whn [THEN [2] bspec])+
|
|
272 |
apply (auto dest: approx_trans3)
|
|
273 |
done
|
|
274 |
|
|
275 |
lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
|
|
276 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)
|
|
277 |
|
|
278 |
|
|
279 |
subsection{*Nslim and Lim*}
|
|
280 |
|
|
281 |
lemma limI: "X ----> L ==> lim X = L"
|
|
282 |
apply (simp add: lim_def)
|
|
283 |
apply (blast intro: LIMSEQ_unique)
|
|
284 |
done
|
|
285 |
|
|
286 |
lemma nslimI: "X ----NS> L ==> nslim X = L"
|
|
287 |
apply (simp add: nslim_def)
|
|
288 |
apply (blast intro: NSLIMSEQ_unique)
|
|
289 |
done
|
|
290 |
|
|
291 |
lemma lim_nslim_iff: "lim X = nslim X"
|
|
292 |
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
|
|
293 |
|
|
294 |
|
|
295 |
subsection{*Convergence*}
|
|
296 |
|
|
297 |
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
|
|
298 |
by (simp add: convergent_def)
|
|
299 |
|
|
300 |
lemma convergentI: "(X ----> L) ==> convergent X"
|
|
301 |
by (auto simp add: convergent_def)
|
|
302 |
|
|
303 |
lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
|
|
304 |
by (simp add: NSconvergent_def)
|
|
305 |
|
|
306 |
lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
|
|
307 |
by (auto simp add: NSconvergent_def)
|
|
308 |
|
|
309 |
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
|
|
310 |
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
|
|
311 |
|
|
312 |
lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
|
|
313 |
by (auto intro: someI simp add: NSconvergent_def nslim_def)
|
|
314 |
|
|
315 |
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
|
|
316 |
by (auto intro: someI simp add: convergent_def lim_def)
|
|
317 |
|
|
318 |
text{*Subsequence (alternative definition, (e.g. Hoskins)*}
|
|
319 |
|
|
320 |
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
|
|
321 |
apply (simp add: subseq_def)
|
|
322 |
apply (auto dest!: less_imp_Suc_add)
|
|
323 |
apply (induct_tac k)
|
|
324 |
apply (auto intro: less_trans)
|
|
325 |
done
|
|
326 |
|
|
327 |
|
|
328 |
subsection{*Monotonicity*}
|
|
329 |
|
|
330 |
lemma monoseq_Suc:
|
|
331 |
"monoseq X = ((\<forall>n. X n \<le> X (Suc n))
|
|
332 |
| (\<forall>n. X (Suc n) \<le> X n))"
|
|
333 |
apply (simp add: monoseq_def)
|
|
334 |
apply (auto dest!: le_imp_less_or_eq)
|
|
335 |
apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
|
|
336 |
apply (induct_tac "ka")
|
|
337 |
apply (auto intro: order_trans)
|
|
338 |
apply (erule swap)
|
|
339 |
apply (induct_tac "k")
|
|
340 |
apply (auto intro: order_trans)
|
|
341 |
done
|
|
342 |
|
|
343 |
lemma monoI1: "\<forall>m n. m \<le> n --> X m \<le> X n ==> monoseq X"
|
|
344 |
by (simp add: monoseq_def)
|
|
345 |
|
|
346 |
lemma monoI2: "\<forall>m n. m \<le> n --> X n \<le> X m ==> monoseq X"
|
|
347 |
by (simp add: monoseq_def)
|
|
348 |
|
|
349 |
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
|
|
350 |
by (simp add: monoseq_Suc)
|
|
351 |
|
|
352 |
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
|
|
353 |
by (simp add: monoseq_Suc)
|
|
354 |
|
|
355 |
|
|
356 |
subsection{*Bounded Sequence*}
|
|
357 |
|
|
358 |
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)"
|
|
359 |
by (simp add: Bseq_def)
|
|
360 |
|
|
361 |
lemma BseqI: "[| 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K |] ==> Bseq X"
|
|
362 |
by (auto simp add: Bseq_def)
|
|
363 |
|
|
364 |
lemma lemma_NBseq_def:
|
|
365 |
"(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
|
|
366 |
(\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
|
|
367 |
apply auto
|
|
368 |
prefer 2 apply force
|
|
369 |
apply (cut_tac x = K in reals_Archimedean2, clarify)
|
|
370 |
apply (rule_tac x = n in exI, clarify)
|
|
371 |
apply (drule_tac x = na in spec)
|
|
372 |
apply (auto simp add: real_of_nat_Suc)
|
|
373 |
done
|
|
374 |
|
|
375 |
text{* alternative definition for Bseq *}
|
|
376 |
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
|
|
377 |
apply (simp add: Bseq_def)
|
|
378 |
apply (simp (no_asm) add: lemma_NBseq_def)
|
|
379 |
done
|
|
380 |
|
|
381 |
lemma lemma_NBseq_def2:
|
|
382 |
"(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
|
|
383 |
(\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
|
|
384 |
apply (subst lemma_NBseq_def, auto)
|
|
385 |
apply (rule_tac x = "Suc N" in exI)
|
|
386 |
apply (rule_tac [2] x = N in exI)
|
|
387 |
apply (auto simp add: real_of_nat_Suc)
|
|
388 |
prefer 2 apply (blast intro: order_less_imp_le)
|
|
389 |
apply (drule_tac x = n in spec, simp)
|
|
390 |
done
|
|
391 |
|
|
392 |
(* yet another definition for Bseq *)
|
|
393 |
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
|
|
394 |
by (simp add: Bseq_def lemma_NBseq_def2)
|
|
395 |
|
|
396 |
lemma NSBseqD: "[| NSBseq X; N: HNatInfinite |] ==> ( *fNat* X) N : HFinite"
|
|
397 |
by (simp add: NSBseq_def)
|
|
398 |
|
|
399 |
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X"
|
|
400 |
by (simp add: NSBseq_def)
|
|
401 |
|
|
402 |
text{*The standard definition implies the nonstandard definition*}
|
|
403 |
|
|
404 |
lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K"
|
|
405 |
by auto
|
|
406 |
|
|
407 |
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
|
|
408 |
apply (simp add: Bseq_def NSBseq_def, safe)
|
|
409 |
apply (rule_tac z = N in eq_Abs_hypnat)
|
|
410 |
apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff
|
|
411 |
HNatInfinite_FreeUltrafilterNat_iff)
|
|
412 |
apply (rule bexI [OF _ lemma_hyprel_refl])
|
|
413 |
apply (drule_tac f = Xa in lemma_Bseq)
|
|
414 |
apply (rule_tac x = "K+1" in exI)
|
|
415 |
apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
|
|
416 |
done
|
|
417 |
|
|
418 |
text{*The nonstandard definition implies the standard definition*}
|
|
419 |
|
|
420 |
(* similar to NSLIM proof in REALTOPOS *)
|
|
421 |
|
|
422 |
text{* We need to get rid of the real variable and do so by proving the
|
|
423 |
following, which relies on the Archimedean property of the reals.
|
|
424 |
When we skolemize we then get the required function @{term "f::nat=>nat"}.
|
|
425 |
Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"}
|
|
426 |
which woulid be useless.*}
|
|
427 |
|
|
428 |
lemma lemmaNSBseq:
|
|
429 |
"\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
|
|
430 |
==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
|
|
431 |
apply safe
|
|
432 |
apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
|
|
433 |
done
|
|
434 |
|
|
435 |
lemma lemmaNSBseq2: "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
|
|
436 |
==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
|
|
437 |
apply (drule lemmaNSBseq)
|
|
438 |
apply (drule choice, blast)
|
|
439 |
done
|
|
440 |
|
|
441 |
lemma real_seq_to_hypreal_HInfinite:
|
|
442 |
"\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
|
|
443 |
==> Abs_hypreal(hyprel``{X o f}) : HInfinite"
|
|
444 |
apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
|
|
445 |
apply (rule bexI [OF _ lemma_hyprel_refl], clarify)
|
|
446 |
apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
|
|
447 |
apply (drule FreeUltrafilterNat_all)
|
|
448 |
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
|
|
449 |
apply (auto simp add: real_of_nat_Suc)
|
|
450 |
done
|
|
451 |
|
|
452 |
text{* Now prove that we can get out an infinite hypernatural as well
|
|
453 |
defined using the skolem function @{term "f::nat=>nat"} above*}
|
|
454 |
|
|
455 |
lemma lemma_finite_NSBseq:
|
|
456 |
"{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le>
|
|
457 |
{n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un
|
|
458 |
{n. real(Suc n) < \<bar>X (Suc u)\<bar>}"
|
|
459 |
by (auto dest!: le_imp_less_or_eq)
|
|
460 |
|
|
461 |
lemma lemma_finite_NSBseq2:
|
|
462 |
"finite {n. f n \<le> (u::nat) & real(Suc n) < \<bar>X(f n)\<bar>}"
|
|
463 |
apply (induct_tac "u")
|
|
464 |
apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
|
|
465 |
apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
|
|
466 |
apply (auto intro: finite_real_of_nat_less_real
|
|
467 |
simp add: real_of_nat_Suc less_diff_eq [symmetric])
|
|
468 |
done
|
|
469 |
|
|
470 |
lemma HNatInfinite_skolem_f:
|
|
471 |
"\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
|
|
472 |
==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite"
|
|
473 |
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
|
|
474 |
apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
|
|
475 |
apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
|
|
476 |
apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE])
|
|
477 |
apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
|
|
478 |
{n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}")
|
|
479 |
apply (erule ssubst)
|
|
480 |
apply (auto simp add: linorder_not_less Compl_def)
|
|
481 |
done
|
|
482 |
|
|
483 |
lemma NSBseq_Bseq: "NSBseq X ==> Bseq X"
|
|
484 |
apply (simp add: Bseq_def NSBseq_def)
|
|
485 |
apply (rule ccontr)
|
|
486 |
apply (auto simp add: linorder_not_less [symmetric])
|
|
487 |
apply (drule lemmaNSBseq2, safe)
|
|
488 |
apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite)
|
|
489 |
apply (drule HNatInfinite_skolem_f [THEN [2] bspec])
|
|
490 |
apply (auto simp add: starfunNat o_def HFinite_HInfinite_iff)
|
|
491 |
done
|
|
492 |
|
|
493 |
text{* Equivalence of nonstandard and standard definitions
|
|
494 |
for a bounded sequence*}
|
|
495 |
lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
|
|
496 |
by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
|
|
497 |
|
|
498 |
text{*A convergent sequence is bounded:
|
|
499 |
Boundedness as a necessary condition for convergence.
|
|
500 |
The nonstandard version has no existential, as usual *}
|
|
501 |
|
|
502 |
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
|
|
503 |
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
|
|
504 |
apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
|
|
505 |
done
|
|
506 |
|
|
507 |
text{*Standard Version: easily now proved using equivalence of NS and
|
|
508 |
standard definitions *}
|
|
509 |
lemma convergent_Bseq: "convergent X ==> Bseq X"
|
|
510 |
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
|
|
511 |
|
|
512 |
|
|
513 |
subsection{*Upper Bounds and Lubs of Bounded Sequences*}
|
|
514 |
|
|
515 |
lemma Bseq_isUb:
|
|
516 |
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
|
|
517 |
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)
|
|
518 |
|
|
519 |
|
|
520 |
text{* Use completeness of reals (supremum property)
|
|
521 |
to show that any bounded sequence has a least upper bound*}
|
|
522 |
|
|
523 |
lemma Bseq_isLub:
|
|
524 |
"!!(X::nat=>real). Bseq X ==>
|
|
525 |
\<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
|
|
526 |
by (blast intro: reals_complete Bseq_isUb)
|
|
527 |
|
|
528 |
lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U"
|
|
529 |
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
|
|
530 |
|
|
531 |
lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U"
|
|
532 |
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
|
|
533 |
|
|
534 |
|
|
535 |
subsection{*A Bounded and Monotonic Sequence Converges*}
|
|
536 |
|
|
537 |
lemma lemma_converg1:
|
|
538 |
"!!(X::nat=>real). [| \<forall>m n. m \<le> n --> X m \<le> X n;
|
|
539 |
isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
|
|
540 |
|] ==> \<forall>n. ma \<le> n --> X n = X ma"
|
|
541 |
apply safe
|
|
542 |
apply (drule_tac y = "X n" in isLubD2)
|
|
543 |
apply (blast dest: order_antisym)+
|
|
544 |
done
|
|
545 |
|
|
546 |
text{* The best of both worlds: Easier to prove this result as a standard
|
|
547 |
theorem and then use equivalence to "transfer" it into the
|
|
548 |
equivalent nonstandard form if needed!*}
|
|
549 |
|
|
550 |
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
|
|
551 |
apply (simp add: LIMSEQ_def)
|
|
552 |
apply (rule_tac x = "X m" in exI, safe)
|
|
553 |
apply (rule_tac x = m in exI, safe)
|
|
554 |
apply (drule spec, erule impE, auto)
|
|
555 |
done
|
|
556 |
|
|
557 |
text{*Now, the same theorem in terms of NS limit *}
|
|
558 |
lemma Bmonoseq_NSLIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----NS> L)"
|
|
559 |
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
|
|
560 |
|
|
561 |
lemma lemma_converg2:
|
|
562 |
"!!(X::nat=>real).
|
|
563 |
[| \<forall>m. X m ~= U; isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
|
|
564 |
apply safe
|
|
565 |
apply (drule_tac y = "X m" in isLubD2)
|
|
566 |
apply (auto dest!: order_le_imp_less_or_eq)
|
|
567 |
done
|
|
568 |
|
|
569 |
lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
|
|
570 |
by (rule setleI [THEN isUbI], auto)
|
|
571 |
|
|
572 |
text{* FIXME: @{term "U - T < U"} is redundant *}
|
|
573 |
lemma lemma_converg4: "!!(X::nat=> real).
|
|
574 |
[| \<forall>m. X m ~= U;
|
|
575 |
isLub UNIV {x. \<exists>n. X n = x} U;
|
|
576 |
0 < T;
|
|
577 |
U + - T < U
|
|
578 |
|] ==> \<exists>m. U + -T < X m & X m < U"
|
|
579 |
apply (drule lemma_converg2, assumption)
|
|
580 |
apply (rule ccontr, simp)
|
|
581 |
apply (simp add: linorder_not_less)
|
|
582 |
apply (drule lemma_converg3)
|
|
583 |
apply (drule isLub_le_isUb, assumption)
|
|
584 |
apply (auto dest: order_less_le_trans)
|
|
585 |
done
|
|
586 |
|
|
587 |
text{*A standard proof of the theorem for monotone increasing sequence*}
|
|
588 |
|
|
589 |
lemma Bseq_mono_convergent:
|
|
590 |
"[| Bseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> convergent X"
|
|
591 |
apply (simp add: convergent_def)
|
|
592 |
apply (frule Bseq_isLub, safe)
|
|
593 |
apply (case_tac "\<exists>m. X m = U", auto)
|
|
594 |
apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
|
|
595 |
(* second case *)
|
|
596 |
apply (rule_tac x = U in exI)
|
|
597 |
apply (subst LIMSEQ_iff, safe)
|
|
598 |
apply (frule lemma_converg2, assumption)
|
|
599 |
apply (drule lemma_converg4, auto)
|
|
600 |
apply (rule_tac x = m in exI, safe)
|
|
601 |
apply (subgoal_tac "X m \<le> X n")
|
|
602 |
prefer 2 apply blast
|
|
603 |
apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
|
|
604 |
done
|
|
605 |
|
|
606 |
text{*Nonstandard version of the theorem*}
|
|
607 |
|
|
608 |
lemma NSBseq_mono_NSconvergent:
|
|
609 |
"[| NSBseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> NSconvergent X"
|
|
610 |
by (auto intro: Bseq_mono_convergent
|
|
611 |
simp add: convergent_NSconvergent_iff [symmetric]
|
|
612 |
Bseq_NSBseq_iff [symmetric])
|
|
613 |
|
|
614 |
lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
|
|
615 |
apply (simp add: convergent_def)
|
|
616 |
apply (auto dest: LIMSEQ_minus)
|
|
617 |
apply (drule LIMSEQ_minus, auto)
|
|
618 |
done
|
|
619 |
|
|
620 |
lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
|
|
621 |
by (simp add: Bseq_def)
|
|
622 |
|
|
623 |
text{*Main monotonicity theorem*}
|
|
624 |
lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
|
|
625 |
apply (simp add: monoseq_def, safe)
|
|
626 |
apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
|
|
627 |
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
|
|
628 |
apply (auto intro!: Bseq_mono_convergent)
|
|
629 |
done
|
|
630 |
|
|
631 |
|
|
632 |
subsection{*A Few More Equivalence Theorems for Boundedness*}
|
|
633 |
|
|
634 |
text{*alternative formulation for boundedness*}
|
|
635 |
lemma Bseq_iff2: "Bseq X = (\<exists>k x. 0 < k & (\<forall>n. \<bar>X(n) + -x\<bar> \<le> k))"
|
|
636 |
apply (unfold Bseq_def, safe)
|
|
637 |
apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
|
|
638 |
apply (rule_tac x = K in exI)
|
|
639 |
apply (rule_tac x = 0 in exI, auto)
|
|
640 |
apply (drule_tac [!] x=n in spec, arith+)
|
|
641 |
done
|
|
642 |
|
|
643 |
text{*alternative formulation for boundedness*}
|
|
644 |
lemma Bseq_iff3: "Bseq X = (\<exists>k N. 0 < k & (\<forall>n. abs(X(n) + -X(N)) \<le> k))"
|
|
645 |
apply safe
|
|
646 |
apply (simp add: Bseq_def, safe)
|
|
647 |
apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
|
|
648 |
apply auto
|
|
649 |
apply arith
|
|
650 |
apply (rule_tac x = N in exI, safe)
|
|
651 |
apply (drule_tac x = n in spec, arith)
|
|
652 |
apply (auto simp add: Bseq_iff2)
|
|
653 |
done
|
|
654 |
|
|
655 |
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
|
|
656 |
apply (simp add: Bseq_def)
|
|
657 |
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI)
|
|
658 |
apply auto
|
|
659 |
apply (drule_tac [2] x = n in spec, arith+)
|
|
660 |
done
|
|
661 |
|
|
662 |
|
|
663 |
subsection{*Equivalence Between NS and Standard Cauchy Sequences*}
|
|
664 |
|
|
665 |
subsubsection{*Standard Implies Nonstandard*}
|
|
666 |
|
|
667 |
lemma lemmaCauchy1:
|
|
668 |
"Abs_hypnat (hypnatrel `` {x}) : HNatInfinite
|
|
669 |
==> {n. M \<le> x n} : FreeUltrafilterNat"
|
|
670 |
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
|
|
671 |
apply (drule_tac x = M in spec, ultra)
|
|
672 |
done
|
|
673 |
|
|
674 |
lemma lemmaCauchy2:
|
|
675 |
"{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
|
|
676 |
{n. M \<le> xa n} Int {n. M \<le> x n} \<le>
|
|
677 |
{n. abs (X (xa n) + - X (x n)) < u}"
|
|
678 |
by blast
|
|
679 |
|
|
680 |
lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
|
|
681 |
apply (simp add: Cauchy_def NSCauchy_def, safe)
|
|
682 |
apply (rule_tac z = M in eq_Abs_hypnat)
|
|
683 |
apply (rule_tac z = N in eq_Abs_hypnat)
|
|
684 |
apply (rule approx_minus_iff [THEN iffD2])
|
|
685 |
apply (rule mem_infmal_iff [THEN iffD1])
|
|
686 |
apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
|
|
687 |
apply (rule bexI, auto)
|
|
688 |
apply (drule spec, auto)
|
|
689 |
apply (drule_tac M = M in lemmaCauchy1)
|
|
690 |
apply (drule_tac M = M in lemmaCauchy1)
|
|
691 |
apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
|
|
692 |
apply (rule FreeUltrafilterNat_Int)
|
|
693 |
apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set)
|
|
694 |
done
|
|
695 |
|
|
696 |
subsubsection{*Nonstandard Implies Standard*}
|
|
697 |
|
|
698 |
lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
|
|
699 |
apply (auto simp add: Cauchy_def NSCauchy_def)
|
|
700 |
apply (rule ccontr, simp)
|
|
701 |
apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)
|
|
702 |
apply (drule bspec, assumption)
|
|
703 |
apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec);
|
|
704 |
apply (auto simp add: starfunNat)
|
|
705 |
apply (drule approx_minus_iff [THEN iffD1])
|
|
706 |
apply (drule mem_infmal_iff [THEN iffD2])
|
|
707 |
apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
|
|
708 |
apply (rename_tac "Y")
|
|
709 |
apply (drule_tac x = e in spec, auto)
|
|
710 |
apply (drule FreeUltrafilterNat_Int, assumption)
|
|
711 |
apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>")
|
|
712 |
prefer 2 apply (erule FreeUltrafilterNat_subset, force)
|
|
713 |
apply (rule FreeUltrafilterNat_empty [THEN notE])
|
|
714 |
apply (subgoal_tac
|
|
715 |
"{n. abs (X (f n) + - X (fa n)) < e} Int
|
|
716 |
{M. ~ abs (X (f M) + - X (fa M)) < e} = {}")
|
|
717 |
apply auto
|
|
718 |
done
|
|
719 |
|
|
720 |
|
|
721 |
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
|
|
722 |
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
|
|
723 |
|
|
724 |
text{*A Cauchy sequence is bounded -- this is the standard
|
|
725 |
proof mechanization rather than the nonstandard proof*}
|
|
726 |
|
|
727 |
lemma lemmaCauchy: "\<forall>n. M \<le> n --> \<bar>X M + - X n\<bar> < (1::real)
|
|
728 |
==> \<forall>n. M \<le> n --> \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
|
|
729 |
apply safe
|
|
730 |
apply (drule spec, auto, arith)
|
|
731 |
done
|
|
732 |
|
|
733 |
lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
|
|
734 |
by auto
|
|
735 |
|
|
736 |
text{* FIXME: Long. Maximal element in subsequence *}
|
|
737 |
lemma SUP_rabs_subseq:
|
|
738 |
"\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
|
|
739 |
apply (induct M)
|
|
740 |
apply (rule_tac x = 0 in exI, simp, safe)
|
|
741 |
apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
|
|
742 |
apply safe
|
|
743 |
apply (rule_tac x = m in exI)
|
|
744 |
apply (rule_tac [2] x = m in exI)
|
|
745 |
apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe)
|
|
746 |
apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE])
|
|
747 |
apply (simp_all add: less_Suc_cancel_iff)
|
|
748 |
apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
|
|
749 |
done
|
|
750 |
|
|
751 |
lemma lemma_Nat_covered:
|
|
752 |
"[| \<forall>m::nat. m \<le> M --> P M m;
|
|
753 |
\<forall>m. M \<le> m --> P M m |]
|
|
754 |
==> \<forall>m. P M m"
|
|
755 |
by (auto elim: less_asym simp add: le_def)
|
|
756 |
|
|
757 |
|
|
758 |
lemma lemma_trans1:
|
|
759 |
"[| \<forall>n. n \<le> M --> \<bar>(X::nat=>real) n\<bar> \<le> a; a < b |]
|
|
760 |
==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
|
|
761 |
by (blast intro: order_le_less_trans [THEN order_less_imp_le])
|
|
762 |
|
|
763 |
lemma lemma_trans2:
|
|
764 |
"[| \<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a; a < b |]
|
|
765 |
==> \<forall>n. M \<le> n --> \<bar>X n\<bar>\<le> b"
|
|
766 |
by (blast intro: order_less_trans [THEN order_less_imp_le])
|
|
767 |
|
|
768 |
lemma lemma_trans3:
|
|
769 |
"[| \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> a; a = b |]
|
|
770 |
==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
|
|
771 |
by auto
|
|
772 |
|
|
773 |
lemma lemma_trans4: "\<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a
|
|
774 |
==> \<forall>n. M \<le> n --> \<bar>X n\<bar> \<le> a"
|
|
775 |
by (blast intro: order_less_imp_le)
|
|
776 |
|
|
777 |
|
|
778 |
text{*Proof is more involved than outlines sketched by various authors
|
|
779 |
would suggest*}
|
|
780 |
|
|
781 |
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
|
|
782 |
apply (simp add: Cauchy_def Bseq_def)
|
|
783 |
apply (drule_tac x = 1 in spec)
|
|
784 |
apply (erule zero_less_one [THEN [2] impE], safe)
|
|
785 |
apply (drule_tac x = M in spec, simp)
|
|
786 |
apply (drule lemmaCauchy)
|
|
787 |
apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
|
|
788 |
apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
|
|
789 |
apply safe
|
|
790 |
apply (drule lemma_trans1, assumption)
|
|
791 |
apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
|
|
792 |
apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
|
|
793 |
apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
|
|
794 |
apply (drule lemma_trans4)
|
|
795 |
apply (drule_tac [2] lemma_trans4)
|
|
796 |
apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
|
|
797 |
apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
|
|
798 |
apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
|
|
799 |
apply (auto elim!: lemma_Nat_covered, arith+)
|
|
800 |
done
|
|
801 |
|
|
802 |
text{*A Cauchy sequence is bounded -- nonstandard version*}
|
|
803 |
|
|
804 |
lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
|
|
805 |
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
|
|
806 |
|
|
807 |
|
|
808 |
text{*Equivalence of Cauchy criterion and convergence:
|
|
809 |
We will prove this using our NS formulation which provides a
|
|
810 |
much easier proof than using the standard definition. We do not
|
|
811 |
need to use properties of subsequences such as boundedness,
|
|
812 |
monotonicity etc... Compare with Harrison's corresponding proof
|
|
813 |
in HOL which is much longer and more complicated. Of course, we do
|
|
814 |
not have problems which he encountered with guessing the right
|
|
815 |
instantiations for his 'espsilon-delta' proof(s) in this case
|
|
816 |
since the NS formulations do not involve existential quantifiers.*}
|
|
817 |
|
|
818 |
lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
|
|
819 |
apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
|
|
820 |
apply (frule NSCauchy_NSBseq)
|
|
821 |
apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
|
|
822 |
apply (drule HNatInfinite_whn [THEN [2] bspec])
|
|
823 |
apply (drule HNatInfinite_whn [THEN [2] bspec])
|
|
824 |
apply (auto dest!: st_part_Ex simp add: SReal_iff)
|
|
825 |
apply (blast intro: approx_trans3)
|
|
826 |
done
|
|
827 |
|
|
828 |
text{*Standard proof for free*}
|
|
829 |
lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
|
|
830 |
by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
|
|
831 |
|
|
832 |
|
|
833 |
text{*We can now try and derive a few properties of sequences,
|
|
834 |
starting with the limit comparison property for sequences.*}
|
|
835 |
|
|
836 |
lemma NSLIMSEQ_le:
|
|
837 |
"[| f ----NS> l; g ----NS> m;
|
|
838 |
\<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n)
|
|
839 |
|] ==> l \<le> m"
|
|
840 |
apply (simp add: NSLIMSEQ_def, safe)
|
|
841 |
apply (drule starfun_le_mono)
|
|
842 |
apply (drule HNatInfinite_whn [THEN [2] bspec])+
|
|
843 |
apply (drule_tac x = whn in spec)
|
|
844 |
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
|
|
845 |
apply clarify
|
|
846 |
apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
|
|
847 |
done
|
|
848 |
|
|
849 |
(* standard version *)
|
|
850 |
lemma LIMSEQ_le:
|
|
851 |
"[| f ----> l; g ----> m; \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n) |]
|
|
852 |
==> l \<le> m"
|
|
853 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
|
|
854 |
|
|
855 |
lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
|
|
856 |
apply (rule LIMSEQ_le)
|
|
857 |
apply (rule LIMSEQ_const, auto)
|
|
858 |
done
|
|
859 |
|
|
860 |
lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
|
|
861 |
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
|
|
862 |
|
|
863 |
lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
|
|
864 |
apply (rule LIMSEQ_le)
|
|
865 |
apply (rule_tac [2] LIMSEQ_const, auto)
|
|
866 |
done
|
|
867 |
|
|
868 |
lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
|
|
869 |
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
|
|
870 |
|
|
871 |
text{*Shift a convergent series by 1:
|
|
872 |
By the equivalence between Cauchiness and convergence and because
|
|
873 |
the successor of an infinite hypernatural is also infinite.*}
|
|
874 |
|
|
875 |
lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
|
|
876 |
apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
|
|
877 |
apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
|
|
878 |
apply (drule bspec, assumption)
|
|
879 |
apply (drule bspec, assumption)
|
|
880 |
apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
|
|
881 |
apply (blast intro: approx_trans3)
|
|
882 |
done
|
|
883 |
|
|
884 |
text{* standard version *}
|
|
885 |
lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
|
|
886 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
|
|
887 |
|
|
888 |
lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
|
|
889 |
apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
|
|
890 |
apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
|
|
891 |
apply (drule bspec, assumption)
|
|
892 |
apply (drule bspec, assumption)
|
|
893 |
apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
|
|
894 |
apply (drule_tac x="N - 1" in bspec)
|
|
895 |
apply (auto intro: approx_trans3)
|
|
896 |
done
|
|
897 |
|
|
898 |
lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
|
|
899 |
apply (simp add: LIMSEQ_NSLIMSEQ_iff)
|
|
900 |
apply (erule NSLIMSEQ_imp_Suc)
|
|
901 |
done
|
|
902 |
|
|
903 |
lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
|
|
904 |
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
|
|
905 |
|
|
906 |
lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
|
|
907 |
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
|
|
908 |
|
|
909 |
text{*A sequence tends to zero iff its abs does*}
|
|
910 |
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
|
|
911 |
by (simp add: LIMSEQ_def)
|
|
912 |
|
|
913 |
text{*We prove the NS version from the standard one, since the NS proof
|
|
914 |
seems more complicated than the standard one above!*}
|
|
915 |
lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
|
|
916 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
|
|
917 |
|
|
918 |
text{*Generalization to other limits*}
|
|
919 |
lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
|
|
920 |
apply (simp add: NSLIMSEQ_def)
|
|
921 |
apply (auto intro: approx_hrabs
|
|
922 |
simp add: starfunNat_rabs hypreal_of_real_hrabs [symmetric])
|
|
923 |
done
|
|
924 |
|
|
925 |
text{* standard version *}
|
|
926 |
lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
|
|
927 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
|
|
928 |
|
|
929 |
text{*An unbounded sequence's inverse tends to 0*}
|
|
930 |
|
|
931 |
text{* standard proof seems easier *}
|
|
932 |
lemma LIMSEQ_inverse_zero:
|
|
933 |
"\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n) ==> (%n. inverse(f n)) ----> 0"
|
|
934 |
apply (simp add: LIMSEQ_def, safe)
|
|
935 |
apply (drule_tac x = "inverse r" in spec, safe)
|
|
936 |
apply (rule_tac x = N in exI, safe)
|
|
937 |
apply (drule spec, auto)
|
|
938 |
apply (frule positive_imp_inverse_positive)
|
|
939 |
apply (frule order_less_trans, assumption)
|
|
940 |
apply (frule_tac a = "f n" in positive_imp_inverse_positive)
|
|
941 |
apply (simp add: abs_if)
|
|
942 |
apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
|
|
943 |
apply (auto intro: inverse_less_iff_less [THEN iffD2]
|
|
944 |
simp del: inverse_inverse_eq)
|
|
945 |
done
|
|
946 |
|
|
947 |
lemma NSLIMSEQ_inverse_zero:
|
|
948 |
"\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n)
|
|
949 |
==> (%n. inverse(f n)) ----NS> 0"
|
|
950 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
|
|
951 |
|
|
952 |
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
|
|
953 |
|
|
954 |
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
|
|
955 |
apply (rule LIMSEQ_inverse_zero, safe)
|
|
956 |
apply (cut_tac x = y in reals_Archimedean2)
|
|
957 |
apply (safe, rule_tac x = n in exI)
|
|
958 |
apply (auto simp add: real_of_nat_Suc)
|
|
959 |
done
|
|
960 |
|
|
961 |
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
|
|
962 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
|
|
963 |
|
|
964 |
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
|
|
965 |
infinity is now easily proved*}
|
|
966 |
|
|
967 |
lemma LIMSEQ_inverse_real_of_nat_add:
|
|
968 |
"(%n. r + inverse(real(Suc n))) ----> r"
|
|
969 |
by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
|
|
970 |
|
|
971 |
lemma NSLIMSEQ_inverse_real_of_nat_add:
|
|
972 |
"(%n. r + inverse(real(Suc n))) ----NS> r"
|
|
973 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
|
|
974 |
|
|
975 |
lemma LIMSEQ_inverse_real_of_nat_add_minus:
|
|
976 |
"(%n. r + -inverse(real(Suc n))) ----> r"
|
|
977 |
by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
|
|
978 |
|
|
979 |
lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
|
|
980 |
"(%n. r + -inverse(real(Suc n))) ----NS> r"
|
|
981 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
|
|
982 |
|
|
983 |
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
|
|
984 |
"(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
|
|
985 |
by (cut_tac b=1 in
|
|
986 |
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
|
|
987 |
|
|
988 |
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
|
|
989 |
"(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
|
|
990 |
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
|
|
991 |
|
|
992 |
|
|
993 |
text{* Real Powers*}
|
|
994 |
|
|
995 |
lemma NSLIMSEQ_pow [rule_format]:
|
|
996 |
"(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
|
|
997 |
apply (induct_tac "m")
|
|
998 |
apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
|
|
999 |
done
|
|
1000 |
|
|
1001 |
lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
|
|
1002 |
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
|
|
1003 |
|
|
1004 |
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
|
|
1005 |
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and
|
|
1006 |
also fact that bounded and monotonic sequence converges.*}
|
|
1007 |
|
|
1008 |
lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
|
|
1009 |
apply (simp add: Bseq_def)
|
|
1010 |
apply (rule_tac x = 1 in exI)
|
|
1011 |
apply (simp add: power_abs)
|
|
1012 |
apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
|
|
1013 |
done
|
|
1014 |
|
|
1015 |
lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
|
|
1016 |
apply (clarify intro!: mono_SucI2)
|
|
1017 |
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
|
|
1018 |
done
|
|
1019 |
|
|
1020 |
lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
|
|
1021 |
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
|
|
1022 |
|
|
1023 |
text{* We now use NS criterion to bring proof of theorem through *}
|
|
1024 |
|
|
1025 |
lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
|
|
1026 |
apply (simp add: NSLIMSEQ_def)
|
|
1027 |
apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
|
|
1028 |
apply (frule NSconvergentD)
|
|
1029 |
apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_pow)
|
|
1030 |
apply (frule HNatInfinite_add_one)
|
|
1031 |
apply (drule bspec, assumption)
|
|
1032 |
apply (drule bspec, assumption)
|
|
1033 |
apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
|
|
1034 |
apply (simp add: hyperpow_add)
|
|
1035 |
apply (drule approx_mult_subst_SReal, assumption)
|
|
1036 |
apply (drule approx_trans3, assumption)
|
|
1037 |
apply (auto simp del: hypreal_of_real_mult simp add: hypreal_of_real_mult [symmetric])
|
|
1038 |
done
|
|
1039 |
|
|
1040 |
text{* standard version *}
|
|
1041 |
lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
|
|
1042 |
by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
|
|
1043 |
|
|
1044 |
lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
|
|
1045 |
apply (cut_tac a = a and x1 = "inverse x" in
|
|
1046 |
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
|
|
1047 |
apply (auto simp add: divide_inverse power_inverse)
|
|
1048 |
apply (simp add: inverse_eq_divide pos_divide_less_eq)
|
|
1049 |
done
|
|
1050 |
|
|
1051 |
subsubsection{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
|
|
1052 |
|
|
1053 |
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
|
|
1054 |
by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
|
|
1055 |
|
|
1056 |
lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
|
|
1057 |
by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
|
|
1058 |
|
|
1059 |
lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
|
|
1060 |
apply (rule LIMSEQ_rabs_zero [THEN iffD1])
|
|
1061 |
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
|
|
1062 |
done
|
|
1063 |
|
|
1064 |
lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
|
|
1065 |
by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
|
|
1066 |
|
|
1067 |
subsection{*Hyperreals and Sequences*}
|
|
1068 |
|
|
1069 |
text{*A bounded sequence is a finite hyperreal*}
|
|
1070 |
lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite"
|
|
1071 |
by (auto intro!: bexI lemma_hyprel_refl
|
|
1072 |
intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
|
|
1073 |
simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
|
|
1074 |
Bseq_iff1a)
|
|
1075 |
|
|
1076 |
text{*A sequence converging to zero defines an infinitesimal*}
|
|
1077 |
lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
|
|
1078 |
"X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal"
|
|
1079 |
apply (simp add: NSLIMSEQ_def)
|
|
1080 |
apply (drule_tac x = whn in bspec)
|
|
1081 |
apply (simp add: HNatInfinite_whn)
|
|
1082 |
apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfunNat)
|
|
1083 |
done
|
|
1084 |
|
|
1085 |
(***---------------------------------------------------------------
|
|
1086 |
Theorems proved by Harrison in HOL that we do not need
|
|
1087 |
in order to prove equivalence between Cauchy criterion
|
|
1088 |
and convergence:
|
|
1089 |
-- Show that every sequence contains a monotonic subsequence
|
|
1090 |
Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
|
|
1091 |
-- Show that a subsequence of a bounded sequence is bounded
|
|
1092 |
Goal "Bseq X ==> Bseq (%n. X (f n))";
|
|
1093 |
-- Show we can take subsequential terms arbitrarily far
|
|
1094 |
up a sequence
|
|
1095 |
Goal "subseq f ==> n \<le> f(n)";
|
|
1096 |
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
|
|
1097 |
---------------------------------------------------------------***)
|
|
1098 |
|
|
1099 |
ML
|
|
1100 |
{*
|
|
1101 |
val Cauchy_def = thm"Cauchy_def";
|
|
1102 |
val SEQ_Infinitesimal = thm "SEQ_Infinitesimal";
|
|
1103 |
val LIMSEQ_iff = thm "LIMSEQ_iff";
|
|
1104 |
val NSLIMSEQ_iff = thm "NSLIMSEQ_iff";
|
|
1105 |
val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ";
|
|
1106 |
val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set";
|
|
1107 |
val Compl_less_set = thm "Compl_less_set";
|
|
1108 |
val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ";
|
|
1109 |
val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ";
|
|
1110 |
val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ";
|
|
1111 |
val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff";
|
|
1112 |
val NSLIMSEQ_const = thm "NSLIMSEQ_const";
|
|
1113 |
val LIMSEQ_const = thm "LIMSEQ_const";
|
|
1114 |
val NSLIMSEQ_add = thm "NSLIMSEQ_add";
|
|
1115 |
val LIMSEQ_add = thm "LIMSEQ_add";
|
|
1116 |
val NSLIMSEQ_mult = thm "NSLIMSEQ_mult";
|
|
1117 |
val LIMSEQ_mult = thm "LIMSEQ_mult";
|
|
1118 |
val NSLIMSEQ_minus = thm "NSLIMSEQ_minus";
|
|
1119 |
val LIMSEQ_minus = thm "LIMSEQ_minus";
|
|
1120 |
val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel";
|
|
1121 |
val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel";
|
|
1122 |
val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus";
|
|
1123 |
val LIMSEQ_add_minus = thm "LIMSEQ_add_minus";
|
|
1124 |
val LIMSEQ_diff = thm "LIMSEQ_diff";
|
|
1125 |
val NSLIMSEQ_diff = thm "NSLIMSEQ_diff";
|
|
1126 |
val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse";
|
|
1127 |
val LIMSEQ_inverse = thm "LIMSEQ_inverse";
|
|
1128 |
val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse";
|
|
1129 |
val LIMSEQ_divide = thm "LIMSEQ_divide";
|
|
1130 |
val NSLIMSEQ_unique = thm "NSLIMSEQ_unique";
|
|
1131 |
val LIMSEQ_unique = thm "LIMSEQ_unique";
|
|
1132 |
val limI = thm "limI";
|
|
1133 |
val nslimI = thm "nslimI";
|
|
1134 |
val lim_nslim_iff = thm "lim_nslim_iff";
|
|
1135 |
val convergentD = thm "convergentD";
|
|
1136 |
val convergentI = thm "convergentI";
|
|
1137 |
val NSconvergentD = thm "NSconvergentD";
|
|
1138 |
val NSconvergentI = thm "NSconvergentI";
|
|
1139 |
val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff";
|
|
1140 |
val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff";
|
|
1141 |
val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff";
|
|
1142 |
val subseq_Suc_iff = thm "subseq_Suc_iff";
|
|
1143 |
val monoseq_Suc = thm "monoseq_Suc";
|
|
1144 |
val monoI1 = thm "monoI1";
|
|
1145 |
val monoI2 = thm "monoI2";
|
|
1146 |
val mono_SucI1 = thm "mono_SucI1";
|
|
1147 |
val mono_SucI2 = thm "mono_SucI2";
|
|
1148 |
val BseqD = thm "BseqD";
|
|
1149 |
val BseqI = thm "BseqI";
|
|
1150 |
val Bseq_iff = thm "Bseq_iff";
|
|
1151 |
val Bseq_iff1a = thm "Bseq_iff1a";
|
|
1152 |
val NSBseqD = thm "NSBseqD";
|
|
1153 |
val NSBseqI = thm "NSBseqI";
|
|
1154 |
val Bseq_NSBseq = thm "Bseq_NSBseq";
|
|
1155 |
val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite";
|
|
1156 |
val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f";
|
|
1157 |
val NSBseq_Bseq = thm "NSBseq_Bseq";
|
|
1158 |
val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff";
|
|
1159 |
val NSconvergent_NSBseq = thm "NSconvergent_NSBseq";
|
|
1160 |
val convergent_Bseq = thm "convergent_Bseq";
|
|
1161 |
val Bseq_isUb = thm "Bseq_isUb";
|
|
1162 |
val Bseq_isLub = thm "Bseq_isLub";
|
|
1163 |
val NSBseq_isUb = thm "NSBseq_isUb";
|
|
1164 |
val NSBseq_isLub = thm "NSBseq_isLub";
|
|
1165 |
val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ";
|
|
1166 |
val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ";
|
|
1167 |
val Bseq_mono_convergent = thm "Bseq_mono_convergent";
|
|
1168 |
val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent";
|
|
1169 |
val convergent_minus_iff = thm "convergent_minus_iff";
|
|
1170 |
val Bseq_minus_iff = thm "Bseq_minus_iff";
|
|
1171 |
val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent";
|
|
1172 |
val Bseq_iff2 = thm "Bseq_iff2";
|
|
1173 |
val Bseq_iff3 = thm "Bseq_iff3";
|
|
1174 |
val BseqI2 = thm "BseqI2";
|
|
1175 |
val Cauchy_NSCauchy = thm "Cauchy_NSCauchy";
|
|
1176 |
val NSCauchy_Cauchy = thm "NSCauchy_Cauchy";
|
|
1177 |
val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff";
|
|
1178 |
val less_Suc_cancel_iff = thm "less_Suc_cancel_iff";
|
|
1179 |
val SUP_rabs_subseq = thm "SUP_rabs_subseq";
|
|
1180 |
val Cauchy_Bseq = thm "Cauchy_Bseq";
|
|
1181 |
val NSCauchy_NSBseq = thm "NSCauchy_NSBseq";
|
|
1182 |
val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff";
|
|
1183 |
val Cauchy_convergent_iff = thm "Cauchy_convergent_iff";
|
|
1184 |
val NSLIMSEQ_le = thm "NSLIMSEQ_le";
|
|
1185 |
val LIMSEQ_le = thm "LIMSEQ_le";
|
|
1186 |
val LIMSEQ_le_const = thm "LIMSEQ_le_const";
|
|
1187 |
val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const";
|
|
1188 |
val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2";
|
|
1189 |
val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2";
|
|
1190 |
val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc";
|
|
1191 |
val LIMSEQ_Suc = thm "LIMSEQ_Suc";
|
|
1192 |
val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc";
|
|
1193 |
val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc";
|
|
1194 |
val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff";
|
|
1195 |
val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff";
|
|
1196 |
val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero";
|
|
1197 |
val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero";
|
|
1198 |
val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs";
|
|
1199 |
val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs";
|
|
1200 |
val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero";
|
|
1201 |
val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero";
|
|
1202 |
val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat";
|
|
1203 |
val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat";
|
|
1204 |
val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add";
|
|
1205 |
val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add";
|
|
1206 |
val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus";
|
|
1207 |
val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus";
|
|
1208 |
val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult";
|
|
1209 |
val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
|
|
1210 |
val NSLIMSEQ_pow = thm "NSLIMSEQ_pow";
|
|
1211 |
val LIMSEQ_pow = thm "LIMSEQ_pow";
|
|
1212 |
val Bseq_realpow = thm "Bseq_realpow";
|
|
1213 |
val monoseq_realpow = thm "monoseq_realpow";
|
|
1214 |
val convergent_realpow = thm "convergent_realpow";
|
|
1215 |
val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
|
|
1216 |
val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero";
|
|
1217 |
val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero";
|
|
1218 |
val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero";
|
|
1219 |
val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero";
|
|
1220 |
val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2";
|
|
1221 |
val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2";
|
|
1222 |
val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal";
|
|
1223 |
val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal";
|
|
1224 |
*}
|
|
1225 |
|
10751
|
1226 |
end
|
|
1227 |
|