10690
|
1 |
(* Title : HSeries.ML
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
4 |
Description : Finite summation and infinite series
|
|
5 |
for hyperreals
|
|
6 |
*)
|
|
7 |
|
|
8 |
Goalw [sumhr_def]
|
|
9 |
"sumhr(M,N,f) = Abs_hypreal(UN X:Rep_hypnat(M). \
|
|
10 |
\ UN Y: Rep_hypnat(N). \
|
|
11 |
\ hyprel ^^{%n::nat. sumr (X n) (Y n) f})";
|
|
12 |
by (Auto_tac);
|
|
13 |
qed "sumhr_iff";
|
|
14 |
|
|
15 |
Goalw [sumhr_def]
|
|
16 |
"sumhr(Abs_hypnat(hypnatrel^^{%n. M n}), \
|
|
17 |
\ Abs_hypnat(hypnatrel^^{%n. N n}),f) = \
|
|
18 |
\ Abs_hypreal(hyprel ^^ {%n. sumr (M n) (N n) f})";
|
|
19 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
20 |
by (Auto_tac THEN Ultra_tac 1);
|
|
21 |
qed "sumhr";
|
|
22 |
|
|
23 |
(*-------------------------------------------------------
|
|
24 |
lcp's suggestion: exploit pattern matching
|
|
25 |
facilities and use as definition instead (to do)
|
|
26 |
-------------------------------------------------------*)
|
|
27 |
Goalw [sumhr_def]
|
|
28 |
"sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \
|
|
29 |
\ UN Y: Rep_hypnat(N). \
|
|
30 |
\ hyprel ^^{%n::nat. sumr (X n) (Y n) f})) p";
|
|
31 |
by (res_inst_tac [("p","p")] PairE 1);
|
|
32 |
by (res_inst_tac [("p","y")] PairE 1);
|
|
33 |
by (Auto_tac);
|
|
34 |
qed "sumhr_iff2";
|
|
35 |
|
|
36 |
(* Theorem corresponding to base case in def of sumr *)
|
|
37 |
Goalw [hypnat_zero_def,hypreal_zero_def]
|
|
38 |
"sumhr (m,0,f) = 0";
|
|
39 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
40 |
by (auto_tac (claset(),simpset() addsimps [sumhr]));
|
|
41 |
qed "sumhr_zero";
|
|
42 |
Addsimps [sumhr_zero];
|
|
43 |
|
|
44 |
(* Theorem corresponding to recursive case in def of sumr *)
|
|
45 |
Goalw [hypnat_one_def,hypreal_zero_def]
|
|
46 |
"sumhr(m,n+1hn,f) = (if n + 1hn <= m then 0 \
|
|
47 |
\ else sumhr(m,n,f) + (*fNat* f) n)";
|
|
48 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
49 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
50 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
51 |
hypnat_add,hypnat_le,starfunNat,hypreal_add]));
|
|
52 |
by (ALLGOALS(Ultra_tac));
|
|
53 |
qed "sumhr_if";
|
|
54 |
|
|
55 |
Goalw [hypnat_one_def,hypreal_zero_def]
|
|
56 |
"sumhr (n + 1hn, n, f) = 0";
|
|
57 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
58 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
59 |
hypnat_add]));
|
|
60 |
qed "sumhr_Suc_zero";
|
|
61 |
Addsimps [sumhr_Suc_zero];
|
|
62 |
|
|
63 |
Goalw [hypreal_zero_def]
|
|
64 |
"sumhr (n,n,f) = 0";
|
|
65 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
66 |
by (auto_tac (claset(), simpset() addsimps [sumhr]));
|
|
67 |
qed "sumhr_eq_bounds";
|
|
68 |
Addsimps [sumhr_eq_bounds];
|
|
69 |
|
|
70 |
Goalw [hypnat_one_def]
|
|
71 |
"sumhr (m,m + 1hn,f) = (*fNat* f) m";
|
|
72 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
73 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
74 |
hypnat_add,starfunNat]));
|
|
75 |
qed "sumhr_Suc";
|
|
76 |
Addsimps [sumhr_Suc];
|
|
77 |
|
|
78 |
Goalw [hypreal_zero_def]
|
|
79 |
"sumhr(m+k,k,f) = 0";
|
|
80 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
81 |
by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
|
|
82 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
83 |
hypnat_add]));
|
|
84 |
qed "sumhr_add_lbound_zero";
|
|
85 |
Addsimps [sumhr_add_lbound_zero];
|
|
86 |
|
|
87 |
Goal "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)";
|
|
88 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
89 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
90 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
91 |
hypreal_add,sumr_add]));
|
|
92 |
qed "sumhr_add";
|
|
93 |
|
|
94 |
Goalw [hypreal_of_real_def]
|
|
95 |
"hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)";
|
|
96 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
97 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
98 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
99 |
hypreal_mult,sumr_mult]));
|
|
100 |
qed "sumhr_mult";
|
|
101 |
|
|
102 |
Goalw [hypnat_zero_def]
|
|
103 |
"n < p ==> sumhr (0,n,f) + sumhr (n,p,f) = sumhr (0,p,f)";
|
|
104 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
105 |
by (res_inst_tac [("z","p")] eq_Abs_hypnat 1);
|
|
106 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset],
|
|
107 |
simpset() addsimps [sumhr,hypreal_add,hypnat_less,
|
|
108 |
sumr_split_add]));
|
|
109 |
qed "sumhr_split_add";
|
|
110 |
|
|
111 |
Goal
|
|
112 |
"n < p ==> sumhr (0, p, f) + \
|
|
113 |
\ - sumhr (0, n, f) = sumhr (n,p,f)";
|
|
114 |
by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1);
|
|
115 |
by (asm_simp_tac (simpset() addsimps hypreal_add_ac) 1);
|
|
116 |
qed "sumhr_split_add_minus";
|
|
117 |
|
|
118 |
Goal "abs(sumhr(m,n,f)) <= sumhr(m,n,%i. abs(f i))";
|
|
119 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
120 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
121 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
122 |
hypreal_le,hypreal_hrabs,sumr_rabs]));
|
|
123 |
qed "sumhr_hrabs";
|
|
124 |
|
|
125 |
(* other general version also needed *)
|
|
126 |
Goalw [hypnat_of_nat_def]
|
|
127 |
"!!f g. (ALL r. m <= r & r < n --> f r = g r) \
|
|
128 |
\ --> sumhr(hypnat_of_nat m,hypnat_of_nat n,f) = sumhr(hypnat_of_nat m,hypnat_of_nat n,g)";
|
|
129 |
by (Step_tac 1 THEN dtac sumr_fun_eq 1);
|
|
130 |
by (auto_tac (claset(),simpset() addsimps [sumhr]));
|
|
131 |
qed "sumhr_fun_hypnat_eq";
|
|
132 |
|
|
133 |
Goalw [hypnat_zero_def,hypreal_of_real_def]
|
|
134 |
"sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r";
|
|
135 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
136 |
by (asm_simp_tac (simpset() addsimps [sumhr,
|
|
137 |
hypreal_of_hypnat,hypreal_mult]) 1);
|
|
138 |
qed "sumhr_const";
|
|
139 |
|
|
140 |
Goalw [hypnat_zero_def,hypreal_of_real_def]
|
|
141 |
"sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) = \
|
|
142 |
\ sumhr(0,n,%i. f i + -r)";
|
|
143 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
144 |
by (asm_simp_tac (simpset() addsimps [sumhr,
|
|
145 |
hypreal_of_hypnat,hypreal_mult,hypreal_add,
|
|
146 |
hypreal_minus,sumr_add RS sym]) 1);
|
|
147 |
qed "sumhr_add_mult_const";
|
|
148 |
|
|
149 |
Goalw [hypreal_zero_def]
|
|
150 |
"n < m ==> sumhr (m,n,f) = 0";
|
|
151 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
152 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
153 |
by (auto_tac (claset() addEs [FreeUltrafilterNat_subset],
|
|
154 |
simpset() addsimps [sumhr,hypnat_less]));
|
|
155 |
qed "sumhr_less_bounds_zero";
|
|
156 |
Addsimps [sumhr_less_bounds_zero];
|
|
157 |
|
|
158 |
Goal "sumhr(m,n,%i. - f i) = - sumhr(m,n,f)";
|
|
159 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
160 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
161 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
162 |
hypreal_minus,sumr_minus]));
|
|
163 |
qed "sumhr_minus";
|
|
164 |
|
|
165 |
Goalw [hypnat_of_nat_def]
|
|
166 |
"sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
|
|
167 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
|
168 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
|
169 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
170 |
hypnat_add,sumr_shift_bounds]));
|
|
171 |
qed "sumhr_shift_bounds";
|
|
172 |
|
|
173 |
(*------------------------------------------------------------------
|
|
174 |
Theorems about NS sums - infinite sums are obtained
|
|
175 |
by summing to some infinite hypernatural (such as whn)
|
|
176 |
-----------------------------------------------------------------*)
|
|
177 |
Goalw [hypnat_omega_def,hypnat_zero_def]
|
|
178 |
"sumhr(0,whn,%i. #1) = hypreal_of_hypnat whn";
|
|
179 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
180 |
hypreal_of_hypnat]));
|
|
181 |
qed "sumhr_hypreal_of_hypnat_omega";
|
|
182 |
|
|
183 |
Goalw [hypnat_omega_def,hypnat_zero_def,
|
|
184 |
hypreal_one_def,omega_def]
|
|
185 |
"sumhr(0,whn,%i. #1) = whr + -1hr";
|
|
186 |
by (auto_tac (claset(),simpset() addsimps [sumhr,
|
|
187 |
real_of_nat_def,hypreal_minus,hypreal_add]));
|
|
188 |
qed "sumhr_hypreal_omega_minus_one";
|
|
189 |
|
|
190 |
Goalw [hypnat_zero_def, hypnat_omega_def, hypreal_zero_def]
|
|
191 |
"sumhr(0, whn + whn, %i. (-#1) ^ (i+1)) = 0";
|
|
192 |
by (simp_tac (simpset() addsimps [sumhr,hypnat_add]
|
|
193 |
delsimps [realpow_Suc]) 1);
|
|
194 |
qed "sumhr_minus_one_realpow_zero";
|
|
195 |
Addsimps [sumhr_minus_one_realpow_zero];
|
|
196 |
|
|
197 |
Goalw [hypnat_of_nat_def,hypreal_of_real_def]
|
|
198 |
"(ALL n. m <= Suc n --> f n = r) & m <= na \
|
|
199 |
\ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
|
|
200 |
\ (hypreal_of_nat (na - m) * hypreal_of_real r)";
|
|
201 |
by (auto_tac (claset() addSDs [sumr_interval_const],
|
|
202 |
simpset() addsimps [sumhr,hypreal_of_nat_real_of_nat,
|
|
203 |
hypreal_of_real_def,hypreal_mult]));
|
|
204 |
qed "sumhr_interval_const";
|
|
205 |
|
|
206 |
Goalw [hypnat_zero_def]
|
|
207 |
"(*fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)";
|
|
208 |
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
|
|
209 |
by (asm_full_simp_tac (simpset() addsimps [starfunNat,sumhr]) 1);
|
|
210 |
qed "starfunNat_sumr";
|
|
211 |
|
|
212 |
Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
|
|
213 |
\ ==> abs (sumhr (M, N, f)) @= 0";
|
|
214 |
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
|
|
215 |
by (auto_tac (claset(),simpset() addsimps [inf_close_refl]));
|
|
216 |
by (dtac (inf_close_sym RS (inf_close_minus_iff RS iffD1)) 1);
|
|
217 |
by (auto_tac (claset() addDs [inf_close_hrabs],
|
|
218 |
simpset() addsimps [sumhr_split_add_minus]));
|
|
219 |
qed "sumhr_hrabs_inf_close";
|
|
220 |
Addsimps [sumhr_hrabs_inf_close];
|
|
221 |
|
|
222 |
(*----------------------------------------------------------------
|
|
223 |
infinite sums: Standard and NS theorems
|
|
224 |
----------------------------------------------------------------*)
|
|
225 |
Goalw [sums_def,NSsums_def] "(f sums l) = (f NSsums l)";
|
|
226 |
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
|
|
227 |
qed "sums_NSsums_iff";
|
|
228 |
|
|
229 |
Goalw [summable_def,NSsummable_def]
|
|
230 |
"(summable f) = (NSsummable f)";
|
|
231 |
by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
|
|
232 |
qed "summable_NSsummable_iff";
|
|
233 |
|
|
234 |
Goalw [suminf_def,NSsuminf_def]
|
|
235 |
"(suminf f) = (NSsuminf f)";
|
|
236 |
by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
|
|
237 |
qed "suminf_NSsuminf_iff";
|
|
238 |
|
|
239 |
Goalw [NSsums_def,NSsummable_def]
|
|
240 |
"f NSsums l ==> NSsummable f";
|
|
241 |
by (Blast_tac 1);
|
|
242 |
qed "NSsums_NSsummable";
|
|
243 |
|
|
244 |
Goalw [NSsummable_def,NSsuminf_def]
|
|
245 |
"NSsummable f ==> f NSsums (NSsuminf f)";
|
|
246 |
by (blast_tac (claset() addIs [someI2]) 1);
|
|
247 |
qed "NSsummable_NSsums";
|
|
248 |
|
|
249 |
Goal "f NSsums s ==> (s = NSsuminf f)";
|
|
250 |
by (asm_full_simp_tac
|
|
251 |
(simpset() addsimps [suminf_NSsuminf_iff RS sym,sums_NSsums_iff,
|
|
252 |
sums_unique]) 1);
|
|
253 |
qed "NSsums_unique";
|
|
254 |
|
|
255 |
Goal "ALL m. n <= Suc m --> f(m) = #0 ==> f NSsums (sumr 0 n f)";
|
|
256 |
by (asm_simp_tac (simpset() addsimps [sums_NSsums_iff RS sym, series_zero]) 1);
|
|
257 |
qed "NSseries_zero";
|
|
258 |
|
|
259 |
Goal "NSsummable f = \
|
|
260 |
\ (ALL M: HNatInfinite. ALL N: HNatInfinite. abs (sumhr(M,N,f)) @= 0)";
|
|
261 |
by (auto_tac (claset(),
|
|
262 |
simpset() addsimps [summable_NSsummable_iff RS sym,
|
|
263 |
summable_convergent_sumr_iff, convergent_NSconvergent_iff,
|
|
264 |
NSCauchy_NSconvergent_iff RS sym, NSCauchy_def,
|
|
265 |
starfunNat_sumr]));
|
|
266 |
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
|
|
267 |
by (auto_tac (claset(), simpset() addsimps [inf_close_refl]));
|
|
268 |
by (rtac ((inf_close_minus_iff RS iffD2) RS inf_close_sym) 1);
|
|
269 |
by (rtac (inf_close_minus_iff RS iffD2) 2);
|
|
270 |
by (auto_tac (claset() addDs [inf_close_hrabs_zero_cancel],
|
|
271 |
simpset() addsimps [sumhr_split_add_minus]));
|
|
272 |
qed "NSsummable_NSCauchy";
|
|
273 |
|
|
274 |
(*-------------------------------------------------------------------
|
|
275 |
Terms of a convergent series tend to zero
|
|
276 |
-------------------------------------------------------------------*)
|
|
277 |
Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> #0";
|
|
278 |
by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy]));
|
|
279 |
by (dtac bspec 1 THEN Auto_tac);
|
|
280 |
by (dres_inst_tac [("x","N + 1hn")] bspec 1);
|
|
281 |
by (auto_tac (claset() addIs [HNatInfinite_add_one,
|
|
282 |
inf_close_hrabs_zero_cancel],
|
|
283 |
simpset() addsimps [rename_numerals hypreal_of_real_zero]));
|
|
284 |
qed "NSsummable_NSLIMSEQ_zero";
|
|
285 |
|
|
286 |
(* Easy to prove stsandard case now *)
|
|
287 |
Goal "summable f ==> f ----> #0";
|
|
288 |
by (auto_tac (claset(),
|
|
289 |
simpset() addsimps [summable_NSsummable_iff,
|
|
290 |
LIMSEQ_NSLIMSEQ_iff, NSsummable_NSLIMSEQ_zero]));
|
|
291 |
qed "summable_LIMSEQ_zero";
|
|
292 |
|
|
293 |
(*-------------------------------------------------------------------
|
|
294 |
NS Comparison test
|
|
295 |
-------------------------------------------------------------------*)
|
|
296 |
|
|
297 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
|
|
298 |
\ NSsummable g \
|
|
299 |
\ |] ==> NSsummable f";
|
|
300 |
by (auto_tac (claset() addIs [summable_comparison_test],
|
|
301 |
simpset() addsimps [summable_NSsummable_iff RS sym]));
|
|
302 |
qed "NSsummable_comparison_test";
|
|
303 |
|
|
304 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
|
|
305 |
\ NSsummable g \
|
|
306 |
\ |] ==> NSsummable (%k. abs (f k))";
|
|
307 |
by (rtac NSsummable_comparison_test 1);
|
|
308 |
by (auto_tac (claset(), simpset() addsimps [abs_idempotent]));
|
|
309 |
qed "NSsummable_rabs_comparison_test";
|
|
310 |
|
|
311 |
|
|
312 |
|
|
313 |
|
|
314 |
|
|
315 |
|
|
316 |
|