7 |
7 |
8 Originally demonstrated permutative rewriting, but add_ac is no longer needed |
8 Originally demonstrated permutative rewriting, but add_ac is no longer needed |
9 thanks to new simprocs. |
9 thanks to new simprocs. |
10 *) |
10 *) |
11 |
11 |
12 Addsimps [add_mult_distrib, add_mult_distrib2]; |
12 (*The sum of the first n odd numbers equals n squared.*) |
|
13 Goal "sum (%i. Suc(i+i)) n = n*n"; |
|
14 by (induct_tac "n" 1); |
|
15 by Auto_tac; |
|
16 qed "sum_of_odds"; |
13 |
17 |
14 (*The sum of the first n positive integers equals n(n+1)/2.*) |
18 (*The sum of the first n positive integers equals n(n+1)/2.*) |
15 Goal "2 * sum id (Suc n) = n*Suc(n)"; |
19 Goal "2 * sum id (Suc n) = n*Suc(n)"; |
16 by (induct_tac "n" 1); |
20 by (induct_tac "n" 1); |
17 by Auto_tac; |
21 by Auto_tac; |
18 qed "sum_of_naturals"; |
22 qed "sum_of_naturals"; |
|
23 |
|
24 Addsimps [add_mult_distrib, add_mult_distrib2]; |
19 |
25 |
20 Goal "Suc(Suc(Suc(Suc 2))) * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(2*n)"; |
26 Goal "Suc(Suc(Suc(Suc 2))) * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(2*n)"; |
21 by (induct_tac "n" 1); |
27 by (induct_tac "n" 1); |
22 by Auto_tac; |
28 by Auto_tac; |
23 qed "sum_of_squares"; |
29 qed "sum_of_squares"; |
24 |
30 |
25 Goal "Suc(Suc 2) * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
31 Goal "Suc(Suc 2) * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
26 by (induct_tac "n" 1); |
32 by (induct_tac "n" 1); |
27 by Auto_tac; |
33 by Auto_tac; |
28 qed "sum_of_cubes"; |
34 qed "sum_of_cubes"; |
29 |
|
30 (*The sum of the first n odd numbers equals n squared.*) |
|
31 Goal "sum (%i. Suc(i+i)) n = n*n"; |
|
32 by (induct_tac "n" 1); |
|
33 by Auto_tac; |
|
34 qed "sum_of_odds"; |
|
35 |
|