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