equal
deleted
inserted
replaced
9 |
9 |
10 Addsimps add_ac; |
10 Addsimps add_ac; |
11 Addsimps [add_mult_distrib, add_mult_distrib2]; |
11 Addsimps [add_mult_distrib, add_mult_distrib2]; |
12 |
12 |
13 (*The sum of the first n positive integers equals n(n+1)/2.*) |
13 (*The sum of the first n positive integers equals n(n+1)/2.*) |
14 goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)"; |
14 goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)"; |
15 by (Simp_tac 1); |
15 by (Simp_tac 1); |
16 by (nat_ind_tac "n" 1); |
16 by (nat_ind_tac "n" 1); |
17 by (Simp_tac 1); |
17 by (Simp_tac 1); |
18 by (Asm_simp_tac 1); |
18 by (Asm_simp_tac 1); |
19 qed "sum_of_naturals"; |
19 qed "sum_of_naturals"; |
20 |
20 |
21 goal NatSum.thy |
21 goal NatSum.thy |
22 "Suc(Suc(Suc(Suc 2)))*sum (%i.i*i) (Suc n) = n*Suc(n)*Suc(2*n)"; |
22 "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)"; |
23 by (Simp_tac 1); |
23 by (Simp_tac 1); |
24 by (nat_ind_tac "n" 1); |
24 by (nat_ind_tac "n" 1); |
25 by (Simp_tac 1); |
25 by (Simp_tac 1); |
26 by (Asm_simp_tac 1); |
26 by (Asm_simp_tac 1); |
27 qed "sum_of_squares"; |
27 qed "sum_of_squares"; |
28 |
28 |
29 goal NatSum.thy |
29 goal NatSum.thy |
30 "Suc(Suc 2)*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; |
30 "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; |
31 by (Simp_tac 1); |
31 by (Simp_tac 1); |
32 by (nat_ind_tac "n" 1); |
32 by (nat_ind_tac "n" 1); |
33 by (Simp_tac 1); |
33 by (Simp_tac 1); |
34 by (Asm_simp_tac 1); |
34 by (Asm_simp_tac 1); |
35 qed "sum_of_cubes"; |
35 qed "sum_of_cubes"; |
36 |
36 |
37 (*The sum of the first n odd numbers equals n squared.*) |
37 (*The sum of the first n odd numbers equals n squared.*) |
38 goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n"; |
38 goal NatSum.thy "sum (%i. Suc(i+i)) n = n*n"; |
39 by (nat_ind_tac "n" 1); |
39 by (nat_ind_tac "n" 1); |
40 by (Simp_tac 1); |
40 by (Simp_tac 1); |
41 by (Asm_simp_tac 1); |
41 by (Asm_simp_tac 1); |
42 qed "sum_of_odds"; |
42 qed "sum_of_odds"; |
43 |
43 |