4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 Summing natural numbers, squares and cubes. Could be continued... |
6 Summing natural numbers, squares and cubes. Could be continued... |
7 *) |
7 *) |
8 |
8 |
9 val natsum_ss = arith_ss addsimps |
9 Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac); |
10 ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac); |
|
11 |
10 |
12 (*The sum of the first n positive integers equals n(n+1)/2.*) |
11 (*The sum of the first n positive integers equals n(n+1)/2.*) |
13 goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)"; |
12 goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)"; |
14 by (simp_tac natsum_ss 1); |
13 by (Simp_tac 1); |
15 by (nat_ind_tac "n" 1); |
14 by (nat_ind_tac "n" 1); |
16 by (simp_tac natsum_ss 1); |
15 by (Simp_tac 1); |
17 by (asm_simp_tac natsum_ss 1); |
16 by (Asm_simp_tac 1); |
18 qed "sum_of_naturals"; |
17 qed "sum_of_naturals"; |
19 |
18 |
20 goal NatSum.thy |
19 goal NatSum.thy |
21 "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = \ |
20 "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = \ |
22 \ n*Suc(n)*Suc(Suc(Suc(0))*n)"; |
21 \ n*Suc(n)*Suc(Suc(Suc(0))*n)"; |
23 by (simp_tac natsum_ss 1); |
22 by (Simp_tac 1); |
24 by (nat_ind_tac "n" 1); |
23 by (nat_ind_tac "n" 1); |
25 by (simp_tac natsum_ss 1); |
24 by (Simp_tac 1); |
26 by (asm_simp_tac natsum_ss 1); |
25 by (Asm_simp_tac 1); |
27 qed "sum_of_squares"; |
26 qed "sum_of_squares"; |
28 |
27 |
29 goal NatSum.thy |
28 goal NatSum.thy |
30 "Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; |
29 "Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; |
31 by (simp_tac natsum_ss 1); |
30 by (Simp_tac 1); |
32 by (nat_ind_tac "n" 1); |
31 by (nat_ind_tac "n" 1); |
33 by (simp_tac natsum_ss 1); |
32 by (Simp_tac 1); |
34 by (asm_simp_tac natsum_ss 1); |
33 by (Asm_simp_tac 1); |
35 qed "sum_of_cubes"; |
34 qed "sum_of_cubes"; |
36 |
35 |
37 (*The sum of the first n odd numbers equals n squared.*) |
36 (*The sum of the first n odd numbers equals n squared.*) |
38 goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n"; |
37 goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n"; |
39 by (nat_ind_tac "n" 1); |
38 by (nat_ind_tac "n" 1); |
40 by (simp_tac natsum_ss 1); |
39 by (Simp_tac 1); |
41 by (asm_simp_tac natsum_ss 1); |
40 by (Asm_simp_tac 1); |
42 qed "sum_of_odds"; |
41 qed "sum_of_odds"; |
43 |
42 |