equal
deleted
inserted
replaced
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(Suc(Suc(0))))))*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(Suc(Suc(0))))*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"; |