--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/NatSum.ML Sun Mar 27 16:43:06 1994 +0200
@@ -0,0 +1,31 @@
+(* Title: HOL/ex/natsum.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1994 TU Muenchen
+
+Summing natural numbers, squares and cubes. Could be continued...
+*)
+
+val natsum_ss = arith_ss addsimps
+ ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
+
+goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
+by(nat_ind_tac "n" 1);
+by(simp_tac natsum_ss 1);
+by(asm_full_simp_tac natsum_ss 1);
+result();
+
+goal NatSum.thy
+ "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum(%i.i*i,Suc(n)) = \
+\ n*Suc(n)*Suc(Suc(Suc(0))*n)";
+by(nat_ind_tac "n" 1);
+by(simp_tac natsum_ss 1);
+by(asm_full_simp_tac natsum_ss 1);
+result();
+
+goal NatSum.thy
+ "Suc(Suc(Suc(Suc(0))))*sum(%i.i*i*i,Suc(n)) = n*n*Suc(n)*Suc(n)";
+by(nat_ind_tac "n" 1);
+by(simp_tac natsum_ss 1);
+by(asm_full_simp_tac natsum_ss 1);
+result();