|
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 |
|
|
|
12 |
goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
|
|
65
|
13 |
by (simp_tac natsum_ss 1);
|
|
|
14 |
by (nat_ind_tac "n" 1);
|
|
|
15 |
by (simp_tac natsum_ss 1);
|
|
|
16 |
by (asm_simp_tac natsum_ss 1);
|
|
63
|
17 |
result();
|
|
|
18 |
|
|
|
19 |
goal NatSum.thy
|
|
|
20 |
"Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum(%i.i*i,Suc(n)) = \
|
|
|
21 |
\ n*Suc(n)*Suc(Suc(Suc(0))*n)";
|
|
65
|
22 |
by (simp_tac natsum_ss 1);
|
|
|
23 |
by (nat_ind_tac "n" 1);
|
|
|
24 |
by (simp_tac natsum_ss 1);
|
|
|
25 |
by (asm_simp_tac natsum_ss 1);
|
|
63
|
26 |
result();
|
|
|
27 |
|
|
|
28 |
goal NatSum.thy
|
|
|
29 |
"Suc(Suc(Suc(Suc(0))))*sum(%i.i*i*i,Suc(n)) = n*n*Suc(n)*Suc(n)";
|
|
65
|
30 |
by (simp_tac natsum_ss 1);
|
|
|
31 |
by (nat_ind_tac "n" 1);
|
|
|
32 |
by (simp_tac natsum_ss 1);
|
|
|
33 |
by (asm_simp_tac natsum_ss 1);
|
|
63
|
34 |
result();
|