1465

1 
(* Title: HOL/ex/natsum.ML

969

2 
ID: $Id$

1465

3 
Author: Tobias Nipkow

969

4 
Copyright 1994 TU Muenchen


5 


6 
Summing natural numbers, squares and cubes. Could be continued...


7 
*)


8 

1266

9 
Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);

969

10 


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

1783

12 
goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";

1266

13 
by (Simp_tac 1);

969

14 
by (nat_ind_tac "n" 1);

1266

15 
by (Simp_tac 1);


16 
by (Asm_simp_tac 1);

969

17 
qed "sum_of_naturals";


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)";

1266

22 
by (Simp_tac 1);

969

23 
by (nat_ind_tac "n" 1);

1266

24 
by (Simp_tac 1);


25 
by (Asm_simp_tac 1);

969

26 
qed "sum_of_squares";


27 


28 
goal NatSum.thy


29 
"Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";

1266

30 
by (Simp_tac 1);

969

31 
by (nat_ind_tac "n" 1);

1266

32 
by (Simp_tac 1);


33 
by (Asm_simp_tac 1);

969

34 
qed "sum_of_cubes";


35 


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


37 
goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n";


38 
by (nat_ind_tac "n" 1);

1266

39 
by (Simp_tac 1);


40 
by (Asm_simp_tac 1);

969

41 
qed "sum_of_odds";


42 
