97 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))"; |
98 by (induct_tac "n" 1); |
98 by (induct_tac "n" 1); |
99 by (Auto_tac); |
99 by (Auto_tac); |
100 qed "sumr_shift_bounds"; |
100 qed "sumr_shift_bounds"; |
101 |
101 |
102 (*FIXME: replace*) |
102 Goal "sumr 0 (#2*n) (%i. (#-1) ^ Suc i) = #0"; |
103 Goal "sumr 0 (n + n) (%i. (- #1) ^ Suc i) = #0"; |
|
104 by (induct_tac "n" 1); |
103 by (induct_tac "n" 1); |
105 by (Auto_tac); |
104 by (Auto_tac); |
106 qed "sumr_minus_one_realpow_zero"; |
105 qed "sumr_minus_one_realpow_zero"; |
107 Addsimps [sumr_minus_one_realpow_zero]; |
106 Addsimps [sumr_minus_one_realpow_zero]; |
108 |
|
109 Goal "sumr 0 (n + n) (%i. (#-1) ^ Suc i) = #0"; |
|
110 by (induct_tac "n" 1); |
|
111 by (Auto_tac); |
|
112 qed "sumr_minus_one_realpow_zero2"; |
|
113 Addsimps [sumr_minus_one_realpow_zero2]; |
|
114 |
107 |
115 Goal "m < Suc n ==> Suc n - m = Suc (n - m)"; |
108 Goal "m < Suc n ==> Suc n - m = Suc (n - m)"; |
116 by (dtac less_imp_Suc_add 1); |
109 by (dtac less_imp_Suc_add 1); |
117 by (Auto_tac); |
110 by (Auto_tac); |
118 val Suc_diff_n = result(); |
111 val Suc_diff_n = result(); |
419 qed "series_pos_less"; |
412 qed "series_pos_less"; |
420 |
413 |
421 (*------------------------------------------------------------------- |
414 (*------------------------------------------------------------------- |
422 sum of geometric progression |
415 sum of geometric progression |
423 -------------------------------------------------------------------*) |
416 -------------------------------------------------------------------*) |
424 (* lemma *) |
|
425 |
417 |
426 Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)"; |
418 Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)"; |
427 by (induct_tac "n" 1); |
419 by (induct_tac "n" 1); |
428 by (Auto_tac); |
420 by (Auto_tac); |
429 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1); |
421 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1); |
430 by (auto_tac (claset(), |
422 by (auto_tac (claset(), |
431 simpset() addsimps [real_eq_minus_iff2 RS sym, |
423 simpset() addsimps [real_mult_assoc, real_add_mult_distrib])); |
432 real_mult_assoc, real_add_mult_distrib])); |
|
433 by (auto_tac (claset(), |
424 by (auto_tac (claset(), |
434 simpset() addsimps [real_add_mult_distrib2, |
425 simpset() addsimps [real_add_mult_distrib2, |
435 real_diff_def, real_mult_commute])); |
426 real_diff_def, real_mult_commute])); |
436 qed "sumr_geometric"; |
427 qed "sumr_geometric"; |
437 |
428 |