author  wenzelm 
Mon, 12 Jan 1998 17:26:34 +0100  
changeset 4558  31becfd8d329 
parent 4246  c539e702e1d2 
child 5069  3ea049f7979d 
permissions  rwrr 
1805
10494d0241cd
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1783
diff
changeset

1 
(* Title: HOL/ex/NatSum.ML 
969  2 
ID: $Id$ 
1465  3 
Author: Tobias Nipkow 
969  4 
Copyright 1994 TU Muenchen 
5 

3269  6 
Summing natural numbers, squares and cubes. Could be continued... 
7 
Demonstrates permutative rewriting. 

969  8 
*) 
9 

4558  10 
Delsimprocs nat_cancel; 
3269  11 
Addsimps add_ac; 
12 
Addsimps [add_mult_distrib, add_mult_distrib2]; 

969  13 

14 
(*The sum of the first n positive integers equals n(n+1)/2.*) 

3842  15 
goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)"; 
1266  16 
by (Simp_tac 1); 
4246  17 
by (induct_tac "n" 1); 
1266  18 
by (Simp_tac 1); 
19 
by (Asm_simp_tac 1); 

969  20 
qed "sum_of_naturals"; 
21 

22 
goal NatSum.thy 

3842  23 
"Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)"; 
1266  24 
by (Simp_tac 1); 
4246  25 
by (induct_tac "n" 1); 
1266  26 
by (Simp_tac 1); 
27 
by (Asm_simp_tac 1); 

969  28 
qed "sum_of_squares"; 
29 

30 
goal NatSum.thy 

3842  31 
"Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; 
1266  32 
by (Simp_tac 1); 
4246  33 
by (induct_tac "n" 1); 
1266  34 
by (Simp_tac 1); 
35 
by (Asm_simp_tac 1); 

969  36 
qed "sum_of_cubes"; 
37 

38 
(*The sum of the first n odd numbers equals n squared.*) 

3842  39 
goal NatSum.thy "sum (%i. Suc(i+i)) n = n*n"; 
4246  40 
by (induct_tac "n" 1); 
1266  41 
by (Simp_tac 1); 
42 
by (Asm_simp_tac 1); 

969  43 
qed "sum_of_odds"; 
44 