author | berghofe |
Fri, 11 Jul 2003 14:55:17 +0200 | |
changeset 14102 | 8af7334af4b3 |
parent 12486 | 0ed8bdd883e0 |
child 14288 | d149e3cbdb39 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : Series.ML |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
: 1999 University of Edinburgh |
|
5 |
Description : Finite summation and infinite series |
|
6 |
*) |
|
7 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
8 |
Goal "sumr (Suc n) n f = 0"; |
10751 | 9 |
by (induct_tac "n" 1); |
10 |
by (Auto_tac); |
|
11 |
qed "sumr_Suc_zero"; |
|
12 |
Addsimps [sumr_Suc_zero]; |
|
13 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
14 |
Goal "sumr m m f = 0"; |
10751 | 15 |
by (induct_tac "m" 1); |
16 |
by (Auto_tac); |
|
17 |
qed "sumr_eq_bounds"; |
|
18 |
Addsimps [sumr_eq_bounds]; |
|
19 |
||
20 |
Goal "sumr m (Suc m) f = f(m)"; |
|
21 |
by (Auto_tac); |
|
22 |
qed "sumr_Suc_eq"; |
|
23 |
Addsimps [sumr_Suc_eq]; |
|
24 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
25 |
Goal "sumr (m+k) k f = 0"; |
10751 | 26 |
by (induct_tac "k" 1); |
27 |
by (Auto_tac); |
|
28 |
qed "sumr_add_lbound_zero"; |
|
29 |
Addsimps [sumr_add_lbound_zero]; |
|
30 |
||
31 |
Goal "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"; |
|
32 |
by (induct_tac "n" 1); |
|
33 |
by (auto_tac (claset(),simpset() addsimps real_add_ac)); |
|
34 |
qed "sumr_add"; |
|
35 |
||
36 |
Goal "r * sumr m n f = sumr m n (%n. r * f n)"; |
|
37 |
by (induct_tac "n" 1); |
|
38 |
by (Auto_tac); |
|
39 |
by (auto_tac (claset(),simpset() addsimps |
|
40 |
[real_add_mult_distrib2])); |
|
41 |
qed "sumr_mult"; |
|
42 |
||
43 |
Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f"; |
|
44 |
by (induct_tac "p" 1); |
|
45 |
by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na", |
|
46 |
leI] addDs [le_anti_sym], simpset())); |
|
47 |
qed_spec_mp "sumr_split_add"; |
|
48 |
||
49 |
Goal "n < p ==> sumr 0 p f + \ |
|
50 |
\ - sumr 0 n f = sumr n p f"; |
|
51 |
by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); |
|
52 |
by (asm_simp_tac (simpset() addsimps real_add_ac) 1); |
|
53 |
qed "sumr_split_add_minus"; |
|
54 |
||
12224 | 55 |
Goal "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"; |
56 |
by (induct_tac "p" 1); |
|
57 |
by (auto_tac (claset() addSDs [CLAIM "[| m < Suc n; n <= m |] ==> m = n"], |
|
58 |
simpset())); |
|
59 |
qed_spec_mp "sumr_split_add2"; |
|
60 |
||
61 |
Goal "[| 0<n; n <= p |] ==> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"; |
|
62 |
by (dtac le_imp_less_or_eq 1 THEN Auto_tac); |
|
63 |
by (blast_tac (claset() addIs [sumr_split_add2]) 1); |
|
64 |
qed "sumr_split_add3"; |
|
65 |
||
10751 | 66 |
Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))"; |
67 |
by (induct_tac "n" 1); |
|
68 |
by (auto_tac (claset() addIs [abs_triangle_ineq RS order_trans, |
|
69 |
real_add_le_mono1], |
|
70 |
simpset())); |
|
71 |
qed "sumr_rabs"; |
|
72 |
||
73 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \ |
|
74 |
\ --> sumr m n f = sumr m n g"; |
|
75 |
by (induct_tac "n" 1); |
|
76 |
by (Auto_tac); |
|
77 |
qed_spec_mp "sumr_fun_eq"; |
|
78 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
79 |
Goal "sumr 0 n (%i. r) = real n * r"; |
10751 | 80 |
by (induct_tac "n" 1); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
81 |
by (auto_tac (claset(), |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
82 |
simpset() addsimps [real_add_mult_distrib,real_of_nat_zero, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
83 |
real_of_nat_Suc])); |
10751 | 84 |
qed "sumr_const"; |
85 |
Addsimps [sumr_const]; |
|
86 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
87 |
Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"; |
10751 | 88 |
by (full_simp_tac (simpset() addsimps [sumr_add RS sym, |
12481
ea5d6da573c5
mods due to reorienting and renaming of real_minus_mult_eq1/2
nipkow
parents:
12224
diff
changeset
|
89 |
real_minus_mult_eq2] delsimps [real_mult_minus_eq2]) 1); |
10751 | 90 |
qed "sumr_add_mult_const"; |
91 |
||
92 |
Goalw [real_diff_def] |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
93 |
"sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"; |
10751 | 94 |
by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1); |
95 |
qed "sumr_diff_mult_const"; |
|
96 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
97 |
Goal "n < m --> sumr m n f = 0"; |
10751 | 98 |
by (induct_tac "n" 1); |
99 |
by (auto_tac (claset() addDs [less_imp_le], simpset())); |
|
100 |
qed_spec_mp "sumr_less_bounds_zero"; |
|
101 |
Addsimps [sumr_less_bounds_zero]; |
|
102 |
||
103 |
Goal "sumr m n (%i. - f i) = - sumr m n f"; |
|
104 |
by (induct_tac "n" 1); |
|
105 |
by (case_tac "Suc n <= m" 2); |
|
106 |
by (auto_tac (claset(),simpset() addsimps |
|
107 |
[real_minus_add_distrib])); |
|
108 |
qed "sumr_minus"; |
|
109 |
||
110 |
Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"; |
|
111 |
by (induct_tac "n" 1); |
|
112 |
by (Auto_tac); |
|
113 |
qed "sumr_shift_bounds"; |
|
114 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
115 |
Goal "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"; |
10751 | 116 |
by (induct_tac "n" 1); |
117 |
by (Auto_tac); |
|
118 |
qed "sumr_minus_one_realpow_zero"; |
|
119 |
Addsimps [sumr_minus_one_realpow_zero]; |
|
120 |
||
121 |
Goal "m < Suc n ==> Suc n - m = Suc (n - m)"; |
|
122 |
by (dtac less_imp_Suc_add 1); |
|
123 |
by (Auto_tac); |
|
124 |
val Suc_diff_n = result(); |
|
125 |
||
126 |
Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
127 |
\ --> sumr m na f = (real (na - m) * r)"; |
10751 | 128 |
by (induct_tac "na" 1); |
129 |
by (Step_tac 1); |
|
130 |
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2); |
|
131 |
by (Step_tac 1); |
|
132 |
by (dres_inst_tac [("x","n")] spec 3); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
133 |
by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset())); |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
134 |
by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, Suc_diff_n, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
135 |
real_of_nat_Suc]) 1); |
10751 | 136 |
qed_spec_mp "sumr_interval_const"; |
137 |
||
138 |
Goal "(ALL n. m <= n --> f n = r) & m <= na \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
139 |
\ --> sumr m na f = (real (na - m) * r)"; |
10751 | 140 |
by (induct_tac "na" 1); |
141 |
by (Step_tac 1); |
|
142 |
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2); |
|
143 |
by (Step_tac 1); |
|
144 |
by (dres_inst_tac [("x","n")] spec 3); |
|
145 |
by (auto_tac (claset() addSDs [le_imp_less_or_eq], |
|
146 |
simpset())); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
147 |
by (asm_simp_tac (simpset() addsimps [Suc_diff_n, real_add_mult_distrib, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
148 |
real_of_nat_Suc]) 1); |
10751 | 149 |
qed_spec_mp "sumr_interval_const2"; |
150 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
151 |
Goal "(ALL n. m <= n --> 0 <= f n) & m < k --> sumr 0 m f <= sumr 0 k f"; |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
152 |
by (induct_tac "k" 1); |
10751 | 153 |
by (Step_tac 1); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
154 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le]))); |
10751 | 155 |
by (ALLGOALS(dres_inst_tac [("x","n")] spec)); |
156 |
by (Step_tac 1); |
|
157 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
|
158 |
by (dtac real_add_le_mono 2); |
|
159 |
by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS real_add_le_mono) 1); |
|
160 |
by (Auto_tac); |
|
161 |
qed_spec_mp "sumr_le"; |
|
162 |
||
163 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \ |
|
164 |
\ --> sumr m n f <= sumr m n g"; |
|
165 |
by (induct_tac "n" 1); |
|
166 |
by (auto_tac (claset() addIs [real_add_le_mono], |
|
167 |
simpset() addsimps [le_def])); |
|
168 |
qed_spec_mp "sumr_le2"; |
|
169 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
170 |
Goal "(ALL n. 0 <= f n) --> 0 <= sumr m n f"; |
10751 | 171 |
by (induct_tac "n" 1); |
172 |
by Auto_tac; |
|
173 |
by (dres_inst_tac [("x","n")] spec 1); |
|
174 |
by (arith_tac 1); |
|
175 |
qed_spec_mp "sumr_ge_zero"; |
|
176 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
177 |
Goal "(ALL n. m <= n --> 0 <= f n) --> 0 <= sumr m n f"; |
10751 | 178 |
by (induct_tac "n" 1); |
179 |
by Auto_tac; |
|
180 |
by (dres_inst_tac [("x","n")] spec 1); |
|
181 |
by (arith_tac 1); |
|
182 |
qed_spec_mp "sumr_ge_zero2"; |
|
183 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
184 |
Goal "0 <= sumr m n (%n. abs (f n))"; |
10751 | 185 |
by (induct_tac "n" 1); |
186 |
by Auto_tac; |
|
187 |
by (arith_tac 1); |
|
188 |
qed "sumr_rabs_ge_zero"; |
|
189 |
Addsimps [sumr_rabs_ge_zero]; |
|
190 |
AddSIs [sumr_rabs_ge_zero]; |
|
191 |
||
192 |
Goal "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"; |
|
193 |
by (induct_tac "n" 1); |
|
194 |
by (Auto_tac THEN arith_tac 1); |
|
195 |
qed "rabs_sumr_rabs_cancel"; |
|
196 |
Addsimps [rabs_sumr_rabs_cancel]; |
|
197 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
198 |
Goal "ALL n. N <= n --> f n = 0 \ |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
199 |
\ ==> ALL m n. N <= m --> sumr m n f = 0"; |
10751 | 200 |
by (Step_tac 1); |
201 |
by (induct_tac "n" 1); |
|
202 |
by (Auto_tac); |
|
203 |
qed "sumr_zero"; |
|
204 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
205 |
Goal "ALL n. N <= n --> f (Suc n) = 0 \ |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
206 |
\ ==> ALL m n. Suc N <= m --> sumr m n f = 0"; |
10751 | 207 |
by (rtac sumr_zero 1 THEN Step_tac 1); |
11468 | 208 |
by (case_tac "n" 1); |
209 |
by Auto_tac; |
|
10751 | 210 |
qed "Suc_le_imp_diff_ge2"; |
211 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
212 |
Goal "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0"; |
10751 | 213 |
by (induct_tac "n" 1); |
11468 | 214 |
by (case_tac "n" 2); |
215 |
by Auto_tac; |
|
10751 | 216 |
qed "sumr_one_lb_realpow_zero"; |
217 |
Addsimps [sumr_one_lb_realpow_zero]; |
|
218 |
||
219 |
Goalw [real_diff_def] "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"; |
|
220 |
by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1); |
|
221 |
qed "sumr_diff"; |
|
222 |
||
11468 | 223 |
Goal "(ALL p. m <= p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"; |
10751 | 224 |
by (induct_tac "n" 1); |
225 |
by (Auto_tac); |
|
226 |
qed_spec_mp "sumr_subst"; |
|
227 |
||
228 |
Goal "(ALL p. m <= p & p < m + n --> (f(p) <= K)) \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
229 |
\ --> (sumr m (m + n) f <= (real n * K))"; |
10751 | 230 |
by (induct_tac "n" 1); |
231 |
by (auto_tac (claset() addIs [real_add_le_mono], |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
232 |
simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); |
10751 | 233 |
qed_spec_mp "sumr_bound"; |
234 |
||
235 |
Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
236 |
\ --> (sumr 0 n f <= (real n * K))"; |
10751 | 237 |
by (induct_tac "n" 1); |
238 |
by (auto_tac (claset() addIs [real_add_le_mono], |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
239 |
simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); |
10751 | 240 |
qed_spec_mp "sumr_bound2"; |
241 |
||
242 |
Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"; |
|
243 |
by (subgoal_tac "k = 0 | 0 < k" 1); |
|
244 |
by (Auto_tac); |
|
245 |
by (induct_tac "n" 1); |
|
246 |
by (auto_tac (claset(),simpset() addsimps [sumr_split_add,add_commute])); |
|
247 |
qed "sumr_group"; |
|
248 |
Addsimps [sumr_group]; |
|
249 |
||
250 |
(*------------------------------------------------------------------- |
|
251 |
Infinite sums |
|
252 |
Theorems follow from properties of limits and sums |
|
253 |
-------------------------------------------------------------------*) |
|
254 |
(*---------------------- |
|
255 |
suminf is the sum |
|
256 |
---------------------*) |
|
257 |
Goalw [sums_def,summable_def] |
|
258 |
"f sums l ==> summable f"; |
|
259 |
by (Blast_tac 1); |
|
260 |
qed "sums_summable"; |
|
261 |
||
262 |
Goalw [summable_def,suminf_def] |
|
263 |
"summable f ==> f sums (suminf f)"; |
|
264 |
by (blast_tac (claset() addIs [someI2]) 1); |
|
265 |
qed "summable_sums"; |
|
266 |
||
267 |
Goalw [summable_def,suminf_def,sums_def] |
|
268 |
"summable f ==> (%n. sumr 0 n f) ----> (suminf f)"; |
|
269 |
by (blast_tac (claset() addIs [someI2]) 1); |
|
270 |
qed "summable_sumr_LIMSEQ_suminf"; |
|
271 |
||
272 |
(*------------------- |
|
273 |
sum is unique |
|
274 |
------------------*) |
|
275 |
Goal "f sums s ==> (s = suminf f)"; |
|
276 |
by (forward_tac [sums_summable RS summable_sums] 1); |
|
277 |
by (auto_tac (claset() addSIs [LIMSEQ_unique], |
|
278 |
simpset() addsimps [sums_def])); |
|
279 |
qed "sums_unique"; |
|
280 |
||
281 |
(* |
|
282 |
Goalw [sums_def,LIMSEQ_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
283 |
"(ALL m. n <= Suc m --> f(m) = 0) ==> f sums (sumr 0 n f)"; |
10751 | 284 |
by (Step_tac 1); |
285 |
by (res_inst_tac [("x","n")] exI 1); |
|
12486 | 286 |
by (Step_tac 1 THEN ftac le_imp_less_or_eq 1); |
10751 | 287 |
by (Step_tac 1); |
288 |
by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
|
289 |
by (ALLGOALS (Asm_simp_tac)); |
|
290 |
by (dtac (conjI RS sumr_interval_const) 1); |
|
291 |
by (Auto_tac); |
|
292 |
qed "series_zero"; |
|
293 |
next one was called series_zero2 |
|
294 |
**********************) |
|
295 |
||
296 |
Goalw [sums_def,LIMSEQ_def] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
297 |
"(ALL m. n <= m --> f(m) = 0) ==> f sums (sumr 0 n f)"; |
10751 | 298 |
by (Step_tac 1); |
299 |
by (res_inst_tac [("x","n")] exI 1); |
|
12486 | 300 |
by (Step_tac 1 THEN ftac le_imp_less_or_eq 1); |
10751 | 301 |
by (Step_tac 1); |
302 |
by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
|
303 |
by (ALLGOALS (Asm_simp_tac)); |
|
304 |
by (dtac (conjI RS sumr_interval_const2) 1); |
|
305 |
by (Auto_tac); |
|
306 |
qed "series_zero"; |
|
307 |
||
308 |
Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"; |
|
309 |
by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], |
|
310 |
simpset() addsimps [sumr_mult RS sym])); |
|
311 |
qed "sums_mult"; |
|
312 |
||
313 |
Goal "x sums x' ==> (%n. x(n)/c) sums (x'/c)"; |
|
314 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, sums_mult, |
|
315 |
inst "w" "inverse c" real_mult_commute]) 1); |
|
316 |
qed "sums_divide"; |
|
317 |
||
318 |
Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"; |
|
319 |
by (auto_tac (claset() addIs [LIMSEQ_diff], |
|
320 |
simpset() addsimps [sumr_diff RS sym])); |
|
321 |
qed "sums_diff"; |
|
322 |
||
323 |
Goal "summable f ==> suminf f * c = suminf(%n. f n * c)"; |
|
324 |
by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
|
325 |
simpset() addsimps [real_mult_commute])); |
|
326 |
qed "suminf_mult"; |
|
327 |
||
328 |
Goal "summable f ==> c * suminf f = suminf(%n. c * f n)"; |
|
329 |
by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
|
330 |
simpset())); |
|
331 |
qed "suminf_mult2"; |
|
332 |
||
333 |
Goal "[| summable f; summable g |] \ |
|
334 |
\ ==> suminf f - suminf g = suminf(%n. f n - g n)"; |
|
335 |
by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums], simpset())); |
|
336 |
qed "suminf_diff"; |
|
337 |
||
338 |
Goalw [sums_def] |
|
339 |
"x sums x0 ==> (%n. - x n) sums - x0"; |
|
340 |
by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus])); |
|
341 |
qed "sums_minus"; |
|
342 |
||
343 |
Goal "[|summable f; 0 < k |] \ |
|
344 |
\ ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"; |
|
345 |
by (dtac summable_sums 1); |
|
346 |
by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def])); |
|
347 |
by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); |
|
348 |
by (res_inst_tac [("x","no")] exI 1 THEN Step_tac 1); |
|
349 |
by (dres_inst_tac [("x","n*k")] spec 1); |
|
350 |
by (auto_tac (claset() addSDs [not_leE], simpset())); |
|
351 |
by (dres_inst_tac [("j","no")] less_le_trans 1); |
|
352 |
by (Auto_tac); |
|
353 |
qed "sums_group"; |
|
354 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
355 |
Goal "[|summable f; ALL d. 0 < (f(n + (Suc (Suc 0) * d))) + f(n + ((Suc (Suc 0) * d) + 1))|] \ |
10751 | 356 |
\ ==> sumr 0 n f < suminf f"; |
357 |
by (dtac summable_sums 1); |
|
358 |
by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def])); |
|
359 |
by (dres_inst_tac [("x","f(n) + f(n + 1)")] spec 1); |
|
360 |
by (Auto_tac); |
|
361 |
by (rtac ccontr 2 THEN dtac real_leI 2); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
362 |
by (subgoal_tac "sumr 0 (n + Suc (Suc 0)) f <= sumr 0 (Suc (Suc 0) * (Suc no) + n) f" 2); |
10751 | 363 |
by (induct_tac "no" 3 THEN Simp_tac 3); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
364 |
by (res_inst_tac [("y","sumr 0 (Suc (Suc 0)*(Suc na)+n) f")] order_trans 3); |
10751 | 365 |
by (assume_tac 3); |
366 |
by (dres_inst_tac [("x","Suc na")] spec 3); |
|
367 |
by (dres_inst_tac [("x","0")] spec 1); |
|
368 |
by (Asm_full_simp_tac 1); |
|
369 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 2); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
370 |
by (rotate_tac 1 1 THEN dres_inst_tac [("x","Suc (Suc 0) * (Suc no) + n")] spec 1); |
10751 | 371 |
by (Step_tac 1 THEN Asm_full_simp_tac 1); |
372 |
by (subgoal_tac "suminf f + (f(n) + f(n + 1)) <= \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
373 |
\ sumr 0 (Suc (Suc 0) * (Suc no) + n) f" 1); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
374 |
by (res_inst_tac [("y","sumr 0 (n+ Suc (Suc 0)) f")] order_trans 2); |
10751 | 375 |
by (assume_tac 3); |
376 |
by (res_inst_tac [("y","sumr 0 n f + (f(n) + f(n + 1))")] order_trans 2); |
|
377 |
by (REPEAT(Asm_simp_tac 2)); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
378 |
by (subgoal_tac "suminf f <= sumr 0 (Suc (Suc 0) * (Suc no) + n) f" 1); |
10751 | 379 |
by (res_inst_tac [("y","suminf f + (f(n) + f(n + 1))")] order_trans 2); |
380 |
by (assume_tac 3); |
|
381 |
by (dres_inst_tac [("x","0")] spec 2); |
|
382 |
by (Asm_full_simp_tac 2); |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
383 |
by (subgoal_tac "0 <= sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f" 1); |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
384 |
by (dtac (abs_eqI1) 1 ); |
10751 | 385 |
by (Asm_full_simp_tac 1); |
386 |
by (auto_tac (claset(),simpset() addsimps [real_le_def])); |
|
387 |
qed "sumr_pos_lt_pair"; |
|
388 |
||
389 |
(*----------------------------------------------------------------- |
|
390 |
Summable series of positive terms has limit >= any partial sum |
|
391 |
----------------------------------------------------------------*) |
|
392 |
Goal |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
393 |
"[| summable f; ALL m. n <= m --> 0 <= f(m) |] \ |
10751 | 394 |
\ ==> sumr 0 n f <= suminf f"; |
395 |
by (dtac summable_sums 1); |
|
396 |
by (rewtac sums_def); |
|
397 |
by (cut_inst_tac [("k","sumr 0 n f")] LIMSEQ_const 1); |
|
398 |
by (etac LIMSEQ_le 1 THEN Step_tac 1); |
|
399 |
by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1); |
|
400 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
|
401 |
by (auto_tac (claset() addIs [sumr_le], simpset())); |
|
402 |
qed "series_pos_le"; |
|
403 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
404 |
Goal "[| summable f; ALL m. n <= m --> 0 < f(m) |] \ |
10751 | 405 |
\ ==> sumr 0 n f < suminf f"; |
406 |
by (res_inst_tac [("y","sumr 0 (Suc n) f")] order_less_le_trans 1); |
|
407 |
by (rtac series_pos_le 2); |
|
408 |
by (Auto_tac); |
|
409 |
by (dres_inst_tac [("x","m")] spec 1); |
|
410 |
by (Auto_tac); |
|
411 |
qed "series_pos_less"; |
|
412 |
||
413 |
(*------------------------------------------------------------------- |
|
414 |
sum of geometric progression |
|
415 |
-------------------------------------------------------------------*) |
|
416 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
417 |
Goal "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"; |
10751 | 418 |
by (induct_tac "n" 1); |
419 |
by (Auto_tac); |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
420 |
by (res_inst_tac [("c1","x - 1")] (real_mult_right_cancel RS iffD1) 1); |
10751 | 421 |
by (auto_tac (claset(), |
422 |
simpset() addsimps [real_mult_assoc, real_add_mult_distrib])); |
|
423 |
by (auto_tac (claset(), |
|
424 |
simpset() addsimps [real_add_mult_distrib2, |
|
425 |
real_diff_def, real_mult_commute])); |
|
426 |
qed "sumr_geometric"; |
|
427 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
428 |
Goal "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
429 |
by (case_tac "x = 1" 1); |
10751 | 430 |
by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2], |
431 |
simpset() addsimps [sumr_geometric ,sums_def, |
|
432 |
real_diff_def, real_add_divide_distrib])); |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
433 |
by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1); |
10751 | 434 |
by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1, |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
435 |
real_divide_minus_eq RS sym, real_diff_def]) 2); |
10751 | 436 |
by (etac ssubst 1); |
437 |
by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1); |
|
438 |
by (auto_tac (claset() addIs [LIMSEQ_const], |
|
439 |
simpset() addsimps [real_diff_def, LIMSEQ_rabs_realpow_zero2])); |
|
440 |
qed "geometric_sums"; |
|
441 |
||
442 |
(*------------------------------------------------------------------- |
|
443 |
Cauchy-type criterion for convergence of series (c.f. Harrison) |
|
444 |
-------------------------------------------------------------------*) |
|
445 |
Goalw [summable_def,sums_def,convergent_def] |
|
446 |
"summable f = convergent (%n. sumr 0 n f)"; |
|
447 |
by (Auto_tac); |
|
448 |
qed "summable_convergent_sumr_iff"; |
|
449 |
||
450 |
Goal "summable f = \ |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
451 |
\ (ALL e. 0 < e --> (EX N. ALL m n. N <= m --> abs(sumr m n f) < e))"; |
10751 | 452 |
by (auto_tac (claset(),simpset() addsimps [summable_convergent_sumr_iff, |
453 |
Cauchy_convergent_iff RS sym,Cauchy_def])); |
|
454 |
by (ALLGOALS(dtac spec) THEN Auto_tac); |
|
455 |
by (res_inst_tac [("x","M")] exI 1); |
|
456 |
by (res_inst_tac [("x","N")] exI 2); |
|
457 |
by (Auto_tac); |
|
458 |
by (ALLGOALS(cut_inst_tac [("m","m"),("n","n")] less_linear)); |
|
459 |
by (Auto_tac); |
|
460 |
by (ftac (le_less_trans RS less_imp_le) 1 THEN assume_tac 1); |
|
461 |
by (dres_inst_tac [("x","n")] spec 1); |
|
462 |
by (dres_inst_tac [("x","m")] spec 1); |
|
463 |
by (auto_tac (claset() addIs [(abs_minus_add_cancel RS subst)], |
|
464 |
simpset() addsimps [sumr_split_add_minus,abs_minus_add_cancel])); |
|
465 |
qed "summable_Cauchy"; |
|
466 |
||
467 |
(*------------------------------------------------------------------- |
|
468 |
Terms of a convergent series tend to zero |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
469 |
> Goalw [LIMSEQ_def] "summable f ==> f ----> 0"; |
10751 | 470 |
Proved easily in HSeries after proving nonstandard case. |
471 |
-------------------------------------------------------------------*) |
|
472 |
(*------------------------------------------------------------------- |
|
473 |
Comparison test |
|
474 |
-------------------------------------------------------------------*) |
|
475 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
|
476 |
\ summable g \ |
|
477 |
\ |] ==> summable f"; |
|
478 |
by (auto_tac (claset(),simpset() addsimps [summable_Cauchy])); |
|
479 |
by (dtac spec 1 THEN Auto_tac); |
|
480 |
by (res_inst_tac [("x","N + Na")] exI 1 THEN Auto_tac); |
|
481 |
by (rotate_tac 2 1); |
|
482 |
by (dres_inst_tac [("x","m")] spec 1); |
|
483 |
by (Auto_tac THEN rotate_tac 2 1 THEN dres_inst_tac [("x","n")] spec 1); |
|
484 |
by (res_inst_tac [("y","sumr m n (%k. abs(f k))")] order_le_less_trans 1); |
|
485 |
by (rtac sumr_rabs 1); |
|
486 |
by (res_inst_tac [("y","sumr m n g")] order_le_less_trans 1); |
|
487 |
by (auto_tac (claset() addIs [sumr_le2], |
|
488 |
simpset() addsimps [abs_interval_iff])); |
|
489 |
qed "summable_comparison_test"; |
|
490 |
||
491 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
|
492 |
\ summable g \ |
|
493 |
\ |] ==> summable (%k. abs (f k))"; |
|
494 |
by (rtac summable_comparison_test 1); |
|
495 |
by (auto_tac (claset(),simpset() addsimps [abs_idempotent])); |
|
496 |
qed "summable_rabs_comparison_test"; |
|
497 |
||
498 |
(*------------------------------------------------------------------*) |
|
499 |
(* Limit comparison property for series (c.f. jrh) *) |
|
500 |
(*------------------------------------------------------------------*) |
|
501 |
Goal "[|ALL n. f n <= g n; summable f; summable g |] \ |
|
502 |
\ ==> suminf f <= suminf g"; |
|
503 |
by (REPEAT(dtac summable_sums 1)); |
|
504 |
by (auto_tac (claset() addSIs [LIMSEQ_le], simpset() addsimps [sums_def])); |
|
505 |
by (rtac exI 1); |
|
506 |
by (auto_tac (claset() addSIs [sumr_le2], simpset())); |
|
507 |
qed "summable_le"; |
|
508 |
||
509 |
Goal "[|ALL n. abs(f n) <= g n; summable g |] \ |
|
510 |
\ ==> summable f & suminf f <= suminf g"; |
|
511 |
by (auto_tac (claset() addIs [summable_comparison_test] |
|
512 |
addSIs [summable_le], simpset())); |
|
513 |
by (auto_tac (claset(),simpset() addsimps [abs_le_interval_iff])); |
|
514 |
qed "summable_le2"; |
|
515 |
||
516 |
(*------------------------------------------------------------------- |
|
517 |
Absolute convergence imples normal convergence |
|
518 |
-------------------------------------------------------------------*) |
|
519 |
Goal "summable (%n. abs (f n)) ==> summable f"; |
|
520 |
by (auto_tac (claset(),simpset() addsimps [sumr_rabs,summable_Cauchy])); |
|
521 |
by (dtac spec 1 THEN Auto_tac); |
|
522 |
by (res_inst_tac [("x","N")] exI 1 THEN Auto_tac); |
|
523 |
by (dtac spec 1 THEN Auto_tac); |
|
524 |
by (res_inst_tac [("y","sumr m n (%n. abs(f n))")] order_le_less_trans 1); |
|
525 |
by (auto_tac (claset() addIs [sumr_rabs], simpset())); |
|
526 |
qed "summable_rabs_cancel"; |
|
527 |
||
528 |
(*------------------------------------------------------------------- |
|
529 |
Absolute convergence of series |
|
530 |
-------------------------------------------------------------------*) |
|
531 |
Goal "summable (%n. abs (f n)) ==> abs(suminf f) <= suminf (%n. abs(f n))"; |
|
532 |
by (auto_tac (claset() addIs [LIMSEQ_le,LIMSEQ_imp_rabs,summable_rabs_cancel, |
|
533 |
summable_sumr_LIMSEQ_suminf,sumr_rabs], |
|
534 |
simpset())); |
|
535 |
qed "summable_rabs"; |
|
536 |
||
537 |
(*------------------------------------------------------------------- |
|
538 |
The ratio test |
|
539 |
-------------------------------------------------------------------*) |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
540 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
541 |
Goal "[| c <= 0; abs x <= c * abs y |] ==> x = (0::real)"; |
10751 | 542 |
by (dtac order_le_imp_less_or_eq 1); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
543 |
by Auto_tac; |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
544 |
by (subgoal_tac "0 <= c * abs y" 1); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
545 |
by (arith_tac 2); |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
546 |
by (asm_full_simp_tac (simpset() addsimps [real_0_le_mult_iff]) 1); |
10751 | 547 |
qed "rabs_ratiotest_lemma"; |
548 |
||
549 |
(* lemmas *) |
|
550 |
||
551 |
Goal "(k::nat) <= l ==> (EX n. l = k + n)"; |
|
552 |
by (dtac le_imp_less_or_eq 1); |
|
553 |
by (auto_tac (claset() addDs [less_imp_Suc_add], simpset())); |
|
554 |
qed "le_Suc_ex"; |
|
555 |
||
556 |
Goal "((k::nat) <= l) = (EX n. l = k + n)"; |
|
557 |
by (auto_tac (claset(),simpset() addsimps [le_Suc_ex])); |
|
558 |
qed "le_Suc_ex_iff"; |
|
559 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
560 |
(*All this trouble just to get 0<c *) |
10751 | 561 |
Goal "[| ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \ |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
562 |
\ ==> 0 < c | summable f"; |
10751 | 563 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
564 |
by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1); |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
565 |
by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = 0" 1); |
10751 | 566 |
by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2); |
11468 | 567 |
by (res_inst_tac [("x","Suc N")] exI 1); |
568 |
by (Clarify_tac 1); |
|
10751 | 569 |
by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac); |
570 |
qed "ratio_test_lemma2"; |
|
571 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
572 |
Goal "[| c < 1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \ |
10751 | 573 |
\ ==> summable f"; |
12486 | 574 |
by (ftac ratio_test_lemma2 1); |
10751 | 575 |
by Auto_tac; |
576 |
by (res_inst_tac [("g","%n. (abs (f N)/(c ^ N))*c ^ n")] |
|
577 |
summable_comparison_test 1); |
|
578 |
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1); |
|
579 |
by (dtac (le_Suc_ex_iff RS iffD1) 1); |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
580 |
by (auto_tac (claset(),simpset() addsimps [realpow_add, realpow_not_zero])); |
10751 | 581 |
by (induct_tac "na" 1 THEN Auto_tac); |
582 |
by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1); |
|
10784 | 583 |
by (auto_tac (claset() addIs [real_mult_le_mono1], |
584 |
simpset() addsimps [summable_def])); |
|
10751 | 585 |
by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
586 |
by (res_inst_tac [("x","abs(f N) * (1/(1 - c)) / (c ^ N)")] exI 1); |
10751 | 587 |
by (rtac sums_divide 1); |
588 |
by (rtac sums_mult 1); |
|
589 |
by (auto_tac (claset() addSIs [sums_mult,geometric_sums], |
|
590 |
simpset() addsimps [real_abs_def])); |
|
591 |
qed "ratio_test"; |
|
592 |
||
593 |
||
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
594 |
(*--------------------------------------------------------------------------*) |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
595 |
(* Differentiation of finite sum *) |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
596 |
(*--------------------------------------------------------------------------*) |
10751 | 597 |
|
598 |
Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \ |
|
599 |
\ --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"; |
|
600 |
by (induct_tac "n" 1); |
|
601 |
by (auto_tac (claset() addIs [DERIV_add], simpset())); |
|
12224 | 602 |
qed_spec_mp "DERIV_sumr"; |