44 by (induct_tac "p" 1); |
44 by (induct_tac "p" 1); |
45 by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na", |
45 by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na", |
46 leI] addDs [le_anti_sym], simpset())); |
46 leI] addDs [le_anti_sym], simpset())); |
47 qed_spec_mp "sumr_split_add"; |
47 qed_spec_mp "sumr_split_add"; |
48 |
48 |
49 Goal "!!n. n < p ==> sumr 0 p f + \ |
49 Goal "n < p ==> sumr 0 p f + \ |
50 \ - sumr 0 n f = sumr n p f"; |
50 \ - sumr 0 n f = sumr n p f"; |
51 by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); |
51 by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); |
52 by (asm_simp_tac (simpset() addsimps real_add_ac) 1); |
52 by (asm_simp_tac (simpset() addsimps real_add_ac) 1); |
53 qed "sumr_split_add_minus"; |
53 qed "sumr_split_add_minus"; |
54 |
54 |
74 Goal "sumr 0 n f + -(real_of_nat n*r) = sumr 0 n (%i. f i + -r)"; |
74 Goal "sumr 0 n f + -(real_of_nat n*r) = sumr 0 n (%i. f i + -r)"; |
75 by (full_simp_tac (simpset() addsimps [sumr_add RS sym, |
75 by (full_simp_tac (simpset() addsimps [sumr_add RS sym, |
76 real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1); |
76 real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1); |
77 qed "sumr_add_mult_const"; |
77 qed "sumr_add_mult_const"; |
78 |
78 |
79 goalw Series.thy [real_diff_def] |
79 Goalw [real_diff_def] |
80 "sumr 0 n f - (real_of_nat n*r) = sumr 0 n (%i. f i - r)"; |
80 "sumr 0 n f - (real_of_nat n*r) = sumr 0 n (%i. f i - r)"; |
81 by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1); |
81 by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1); |
82 qed "sumr_diff_mult_const"; |
82 qed "sumr_diff_mult_const"; |
83 |
83 |
84 Goal "n < m --> sumr m n f = #0"; |
84 Goal "n < m --> sumr m n f = #0"; |
91 by (induct_tac "n" 1); |
91 by (induct_tac "n" 1); |
92 by (case_tac "Suc n <= m" 2); |
92 by (case_tac "Suc n <= m" 2); |
93 by (auto_tac (claset(),simpset() addsimps |
93 by (auto_tac (claset(),simpset() addsimps |
94 [real_minus_add_distrib])); |
94 [real_minus_add_distrib])); |
95 qed "sumr_minus"; |
95 qed "sumr_minus"; |
96 |
|
97 context NatArith.thy; |
|
98 |
|
99 Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m"; |
|
100 by (auto_tac (claset() addSDs [not_leE], simpset())); |
|
101 qed "lemma_not_Suc_add"; |
|
102 |
|
103 context thy; |
|
104 |
96 |
105 Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"; |
97 Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"; |
106 by (induct_tac "n" 1); |
98 by (induct_tac "n" 1); |
107 by (Auto_tac); |
99 by (Auto_tac); |
108 qed "sumr_shift_bounds"; |
100 qed "sumr_shift_bounds"; |
176 simpset() addsimps [le_def])); |
168 simpset() addsimps [le_def])); |
177 qed_spec_mp "sumr_le2"; |
169 qed_spec_mp "sumr_le2"; |
178 |
170 |
179 Goal "(ALL n. #0 <= f n) --> #0 <= sumr m n f"; |
171 Goal "(ALL n. #0 <= f n) --> #0 <= sumr m n f"; |
180 by (induct_tac "n" 1); |
172 by (induct_tac "n" 1); |
181 by (auto_tac (claset(),simpset() addsimps |
173 by Auto_tac; |
182 [rename_numerals real_le_add_order])); |
174 by (dres_inst_tac [("x","n")] spec 1); |
|
175 by (arith_tac 1); |
183 qed_spec_mp "sumr_ge_zero"; |
176 qed_spec_mp "sumr_ge_zero"; |
184 |
177 |
185 Goal "(ALL n. m <= n --> #0 <= f n) --> #0 <= sumr m n f"; |
178 Goal "(ALL n. m <= n --> #0 <= f n) --> #0 <= sumr m n f"; |
186 by (induct_tac "n" 1); |
179 by (induct_tac "n" 1); |
187 by (auto_tac (claset() addIs [rename_numerals real_le_add_order] |
180 by Auto_tac; |
188 addDs [leI], simpset())); |
181 by (dres_inst_tac [("x","n")] spec 1); |
|
182 by (arith_tac 1); |
189 qed_spec_mp "sumr_ge_zero2"; |
183 qed_spec_mp "sumr_ge_zero2"; |
190 |
184 |
191 Goal "#0 <= sumr m n (%n. abs (f n))"; |
185 Goal "#0 <= sumr m n (%n. abs (f n))"; |
192 by (induct_tac "n" 1); |
186 by (induct_tac "n" 1); |
193 by (auto_tac (claset() addSIs [rename_numerals real_le_add_order, |
187 by Auto_tac; |
194 abs_ge_zero], simpset())); |
188 by (arith_tac 1); |
195 qed "sumr_rabs_ge_zero"; |
189 qed "sumr_rabs_ge_zero"; |
196 Addsimps [sumr_rabs_ge_zero]; |
190 Addsimps [sumr_rabs_ge_zero]; |
197 AddSIs [sumr_rabs_ge_zero]; |
191 AddSIs [sumr_rabs_ge_zero]; |
198 |
192 |
199 Goal "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"; |
193 Goal "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"; |
277 -------------------------------------------------------------------*) |
271 -------------------------------------------------------------------*) |
278 (*---------------------- |
272 (*---------------------- |
279 suminf is the sum |
273 suminf is the sum |
280 ---------------------*) |
274 ---------------------*) |
281 Goalw [sums_def,summable_def] |
275 Goalw [sums_def,summable_def] |
282 "!!f. f sums l ==> summable f"; |
276 "f sums l ==> summable f"; |
283 by (Blast_tac 1); |
277 by (Blast_tac 1); |
284 qed "sums_summable"; |
278 qed "sums_summable"; |
285 |
279 |
286 Goalw [summable_def,suminf_def] |
280 Goalw [summable_def,suminf_def] |
287 "!!f. summable f ==> f sums (suminf f)"; |
281 "summable f ==> f sums (suminf f)"; |
288 by (blast_tac (claset() addIs [someI2]) 1); |
282 by (blast_tac (claset() addIs [someI2]) 1); |
289 qed "summable_sums"; |
283 qed "summable_sums"; |
290 |
284 |
291 Goalw [summable_def,suminf_def,sums_def] |
285 Goalw [summable_def,suminf_def,sums_def] |
292 "!!f. summable f ==> (%n. sumr 0 n f) ----> (suminf f)"; |
286 "summable f ==> (%n. sumr 0 n f) ----> (suminf f)"; |
293 by (blast_tac (claset() addIs [someI2]) 1); |
287 by (blast_tac (claset() addIs [someI2]) 1); |
294 qed "summable_sumr_LIMSEQ_suminf"; |
288 qed "summable_sumr_LIMSEQ_suminf"; |
295 |
289 |
296 (*------------------- |
290 (*------------------- |
297 sum is unique |
291 sum is unique |
298 ------------------*) |
292 ------------------*) |
299 Goal "!!f. f sums s ==> (s = suminf f)"; |
293 Goal "f sums s ==> (s = suminf f)"; |
300 by (forward_tac [sums_summable RS summable_sums] 1); |
294 by (forward_tac [sums_summable RS summable_sums] 1); |
301 by (auto_tac (claset() addSIs [LIMSEQ_unique], |
295 by (auto_tac (claset() addSIs [LIMSEQ_unique], |
302 simpset() addsimps [sums_def])); |
296 simpset() addsimps [sums_def])); |
303 qed "sums_unique"; |
297 qed "sums_unique"; |
304 |
298 |
|
299 (* |
305 Goalw [sums_def,LIMSEQ_def] |
300 Goalw [sums_def,LIMSEQ_def] |
306 "!!f. ALL m. n <= Suc m --> f(m) = #0 \ |
301 "(ALL m. n <= Suc m --> f(m) = #0) ==> f sums (sumr 0 n f)"; |
307 \ ==> f sums (sumr 0 n f)"; |
|
308 by (Step_tac 1); |
302 by (Step_tac 1); |
309 by (res_inst_tac [("x","n")] exI 1); |
303 by (res_inst_tac [("x","n")] exI 1); |
310 by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
304 by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
311 by (Step_tac 1); |
305 by (Step_tac 1); |
312 by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
306 by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
313 by (ALLGOALS (Asm_simp_tac)); |
307 by (ALLGOALS (Asm_simp_tac)); |
314 by (dtac (conjI RS sumr_interval_const) 1); |
308 by (dtac (conjI RS sumr_interval_const) 1); |
315 by (Auto_tac); |
309 by (Auto_tac); |
316 qed "series_zero"; |
310 qed "series_zero"; |
317 |
311 next one was called series_zero2 |
318 goalw Series.thy [sums_def,LIMSEQ_def] |
312 **********************) |
319 "!!f. ALL m. n <= m --> f(m) = #0 \ |
313 |
320 \ ==> f sums (sumr 0 n f)"; |
314 Goalw [sums_def,LIMSEQ_def] |
|
315 "(ALL m. n <= m --> f(m) = #0) ==> f sums (sumr 0 n f)"; |
321 by (Step_tac 1); |
316 by (Step_tac 1); |
322 by (res_inst_tac [("x","n")] exI 1); |
317 by (res_inst_tac [("x","n")] exI 1); |
323 by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
318 by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
324 by (Step_tac 1); |
319 by (Step_tac 1); |
325 by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
320 by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
326 by (ALLGOALS (Asm_simp_tac)); |
321 by (ALLGOALS (Asm_simp_tac)); |
327 by (dtac (conjI RS sumr_interval_const2) 1); |
322 by (dtac (conjI RS sumr_interval_const2) 1); |
328 by (Auto_tac); |
323 by (Auto_tac); |
329 qed "series_zero2"; |
324 qed "series_zero"; |
330 |
325 |
331 Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"; |
326 Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"; |
332 by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], |
327 by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], |
333 simpset() addsimps [sumr_mult RS sym])); |
328 simpset() addsimps [sumr_mult RS sym])); |
334 qed "sums_mult"; |
329 qed "sums_mult"; |
336 Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0 - y0)"; |
331 Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0 - y0)"; |
337 by (auto_tac (claset() addIs [LIMSEQ_diff], |
332 by (auto_tac (claset() addIs [LIMSEQ_diff], |
338 simpset() addsimps [sumr_diff RS sym])); |
333 simpset() addsimps [sumr_diff RS sym])); |
339 qed "sums_diff"; |
334 qed "sums_diff"; |
340 |
335 |
341 goal Series.thy "!!f. summable f ==> suminf f * c = suminf(%n. f n * c)"; |
336 Goal "summable f ==> suminf f * c = suminf(%n. f n * c)"; |
342 by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
337 by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
343 simpset() addsimps [real_mult_commute])); |
338 simpset() addsimps [real_mult_commute])); |
344 qed "suminf_mult"; |
339 qed "suminf_mult"; |
345 |
340 |
346 goal Series.thy "!!f. summable f ==> c * suminf f = suminf(%n. c * f n)"; |
341 Goal "summable f ==> c * suminf f = suminf(%n. c * f n)"; |
347 by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
342 by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
348 simpset())); |
343 simpset())); |
349 qed "suminf_mult2"; |
344 qed "suminf_mult2"; |
350 |
345 |
351 Goal "[| summable f; summable g |] \ |
346 Goal "[| summable f; summable g |] \ |
352 \ ==> suminf f - suminf g = suminf(%n. f n - g n)"; |
347 \ ==> suminf f - suminf g = suminf(%n. f n - g n)"; |
353 by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums], simpset())); |
348 by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums], simpset())); |
354 qed "suminf_diff"; |
349 qed "suminf_diff"; |
355 |
350 |
356 goalw Series.thy [sums_def] |
351 Goalw [sums_def] |
357 "!!x. x sums x0 ==> (%n. - x n) sums - x0"; |
352 "x sums x0 ==> (%n. - x n) sums - x0"; |
358 by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus])); |
353 by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus])); |
359 qed "sums_minus"; |
354 qed "sums_minus"; |
360 |
355 |
361 Goal "[|summable f; 0 < k |] \ |
356 Goal "[|summable f; 0 < k |] \ |
362 \ ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"; |
357 \ ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"; |
406 |
401 |
407 (*----------------------------------------------------------------- |
402 (*----------------------------------------------------------------- |
408 Summable series of positive terms has limit >= any partial sum |
403 Summable series of positive terms has limit >= any partial sum |
409 ----------------------------------------------------------------*) |
404 ----------------------------------------------------------------*) |
410 Goal |
405 Goal |
411 "!!f. [| summable f; ALL m. n <= m --> #0 <= f(m) |] \ |
406 "[| summable f; ALL m. n <= m --> #0 <= f(m) |] \ |
412 \ ==> sumr 0 n f <= suminf f"; |
407 \ ==> sumr 0 n f <= suminf f"; |
413 by (dtac summable_sums 1); |
408 by (dtac summable_sums 1); |
414 by (rewtac sums_def); |
409 by (rewtac sums_def); |
415 by (cut_inst_tac [("k","sumr 0 n f")] LIMSEQ_const 1); |
410 by (cut_inst_tac [("k","sumr 0 n f")] LIMSEQ_const 1); |
416 by (etac LIMSEQ_le 1 THEN Step_tac 1); |
411 by (etac LIMSEQ_le 1 THEN Step_tac 1); |
417 by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1); |
412 by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1); |
418 by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
413 by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
419 by (auto_tac (claset() addIs [sumr_le], simpset())); |
414 by (auto_tac (claset() addIs [sumr_le], simpset())); |
420 qed "series_pos_le"; |
415 qed "series_pos_le"; |
421 |
416 |
422 Goal "!!f. [| summable f; ALL m. n <= m --> #0 < f(m) |] \ |
417 Goal "[| summable f; ALL m. n <= m --> #0 < f(m) |] \ |
423 \ ==> sumr 0 n f < suminf f"; |
418 \ ==> sumr 0 n f < suminf f"; |
424 by (res_inst_tac [("j","sumr 0 (Suc n) f")] real_less_le_trans 1); |
419 by (res_inst_tac [("j","sumr 0 (Suc n) f")] real_less_le_trans 1); |
425 by (rtac series_pos_le 2); |
420 by (rtac series_pos_le 2); |
426 by (Auto_tac); |
421 by (Auto_tac); |
427 by (dres_inst_tac [("x","m")] spec 1); |
422 by (dres_inst_tac [("x","m")] spec 1); |
431 (*------------------------------------------------------------------- |
426 (*------------------------------------------------------------------- |
432 sum of geometric progression |
427 sum of geometric progression |
433 -------------------------------------------------------------------*) |
428 -------------------------------------------------------------------*) |
434 (* lemma *) |
429 (* lemma *) |
435 |
430 |
436 Goalw [real_diff_def] "x ~= y ==> x - y ~= (#0::real)"; |
|
437 by (asm_full_simp_tac (simpset() addsimps |
|
438 [rename_numerals (real_eq_minus_iff2 RS sym)]) 1); |
|
439 qed "real_not_eq_diff"; |
|
440 |
|
441 Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)"; |
431 Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)"; |
442 by (induct_tac "n" 1); |
432 by (induct_tac "n" 1); |
443 by (Auto_tac); |
433 by (Auto_tac); |
444 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1); |
434 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1); |
445 by (auto_tac (claset(),simpset() addsimps [real_not_eq_diff, |
435 by (auto_tac (claset(), |
446 real_eq_minus_iff2 RS sym,real_mult_assoc,real_add_mult_distrib])); |
436 simpset() addsimps [real_eq_minus_iff2 RS sym, |
447 by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2, |
437 real_mult_assoc, real_add_mult_distrib])); |
448 real_diff_def,real_mult_commute]) 1); |
438 by (auto_tac (claset(), |
|
439 simpset() addsimps [real_add_mult_distrib2, |
|
440 real_diff_def, real_mult_commute])); |
449 qed "sumr_geometric"; |
441 qed "sumr_geometric"; |
450 |
442 |
451 Goal "abs(x) < #1 ==> (%n. x ^ n) sums inverse(#1 - x)"; |
443 Goal "abs(x) < #1 ==> (%n. x ^ n) sums inverse(#1 - x)"; |
452 by (case_tac "x = #1" 1); |
444 by (case_tac "x = #1" 1); |
453 by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2], |
445 by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2], |
454 simpset() addsimps [sumr_geometric,abs_one,sums_def, |
446 simpset() addsimps [sumr_geometric,abs_one,sums_def, |
455 real_diff_def,real_add_mult_distrib])); |
447 real_diff_def,real_add_mult_distrib])); |
456 by (rtac (real_add_zero_left RS subst) 1); |
448 by (rtac (real_add_zero_left RS subst) 1); |
457 by (rtac (real_mult_0 RS subst) 1); |
449 by (rtac (real_mult_0 RS subst) 1); |
458 by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1); |
450 by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1); |
459 by (dtac real_not_eq_diff 3); |
|
460 by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps |
451 by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps |
461 [real_minus_inverse RS sym,real_diff_def,real_add_commute, |
452 [real_minus_inverse RS sym,real_diff_def,real_add_commute, |
462 rename_numerals LIMSEQ_rabs_realpow_zero2])); |
453 rename_numerals LIMSEQ_rabs_realpow_zero2])); |
463 qed "geometric_sums"; |
454 qed "geometric_sums"; |
464 |
455 |