13 Goal "sum (%i. Suc(i+i)) n = n*n"; |
13 Goal "sum (%i. Suc(i+i)) n = n*n"; |
14 by (induct_tac "n" 1); |
14 by (induct_tac "n" 1); |
15 by Auto_tac; |
15 by Auto_tac; |
16 qed "sum_of_odds"; |
16 qed "sum_of_odds"; |
17 |
17 |
18 (*The sum of the first n positive integers equals n(n+1)/2.*) |
|
19 Goal "2 * sum id (Suc n) = n*Suc(n)"; |
|
20 by (induct_tac "n" 1); |
|
21 by Auto_tac; |
|
22 qed "sum_of_naturals"; |
|
23 |
|
24 Addsimps [add_mult_distrib, add_mult_distrib2]; |
18 Addsimps [add_mult_distrib, add_mult_distrib2]; |
25 |
|
26 Goal "Suc(Suc(Suc(Suc 2))) * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(2*n)"; |
|
27 by (induct_tac "n" 1); |
|
28 by Auto_tac; |
|
29 qed "sum_of_squares"; |
|
30 |
|
31 Goal "Suc(Suc 2) * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
|
32 by (induct_tac "n" 1); |
|
33 by Auto_tac; |
|
34 qed "sum_of_cubes"; |
|
35 |
|
36 |
|
37 (** Repeating some of the previous examples using binary numerals **) |
|
38 |
19 |
39 (*The sum of the first n positive integers equals n(n+1)/2.*) |
20 (*The sum of the first n positive integers equals n(n+1)/2.*) |
40 Goal "#2 * sum id (Suc n) = n*Suc(n)"; |
21 Goal "#2 * sum id (Suc n) = n*Suc(n)"; |
41 by (induct_tac "n" 1); |
22 by (induct_tac "n" 1); |
42 by Auto_tac; |
23 by Auto_tac; |
43 qed "sum_of_naturals"; |
24 qed "sum_of_naturals"; |
44 |
25 |
45 Addsimps [add_mult_distrib, add_mult_distrib2]; |
|
46 |
|
47 Goal "#6 * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(#2*n)"; |
26 Goal "#6 * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(#2*n)"; |
48 by (induct_tac "n" 1); |
27 by (induct_tac "n" 1); |
49 by Auto_tac; |
28 by Auto_tac; |
50 (*12.6 secs, down to 5.9 secs, down to 4 secs*) |
|
51 qed "sum_of_squares"; |
29 qed "sum_of_squares"; |
52 |
30 |
53 Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
31 Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
54 by (induct_tac "n" 1); |
32 by (induct_tac "n" 1); |
55 by Auto_tac; |
33 by Auto_tac; |
56 (*27.7 secs, down to 10.9 secs, down to 7.3 secs*) |
|
57 qed "sum_of_cubes"; |
34 qed "sum_of_cubes"; |