# HG changeset patch
# User nipkow
# Date 764779386 -7200
# Node ID 94436622324d5ba94c2af982a9f6f415f6d4fbe8
# Parent  32a83e3ad5a4d62dbc87a8734686f29bc11c1377
Added some sums.

diff -r 32a83e3ad5a4 -r 94436622324d ex/NatSum.ML
--- /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();
diff -r 32a83e3ad5a4 -r 94436622324d ex/NatSum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/NatSum.thy	Sun Mar 27 16:43:06 1994 +0200
@@ -0,0 +1,13 @@
+(*  Title: 	HOL/ex/natsum.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
+*)
+
+NatSum = Arith +
+consts sum :: "[nat=>nat, nat] => nat"
+rules  sum_0   "sum(f,0) = 0"
+       sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
+end
diff -r 32a83e3ad5a4 -r 94436622324d ex/ROOT.ML
--- a/ex/ROOT.ML	Sun Mar 27 12:36:39 1994 +0200
+++ b/ex/ROOT.ML	Sun Mar 27 16:43:06 1994 +0200
@@ -18,6 +18,7 @@
 time_use_thy "Qsort";
 time_use_thy "LexProd";
 time_use_thy "Puzzle";
+time_use_thy "NatSum";
 time_use     "ex/set.ML";
 time_use_thy "PL";
 time_use_thy "Term";
diff -r 32a83e3ad5a4 -r 94436622324d ex/natsum.ML
--- /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();
diff -r 32a83e3ad5a4 -r 94436622324d ex/natsum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/natsum.thy	Sun Mar 27 16:43:06 1994 +0200
@@ -0,0 +1,13 @@
+(*  Title: 	HOL/ex/natsum.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
+*)
+
+NatSum = Arith +
+consts sum :: "[nat=>nat, nat] => nat"
+rules  sum_0   "sum(f,0) = 0"
+       sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
+end
diff -r 32a83e3ad5a4 -r 94436622324d ex/natsum.thy~
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/natsum.thy~	Sun Mar 27 16:43:06 1994 +0200
@@ -0,0 +1,13 @@
+(*  Title: 	HOL/ex/sum.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994 TU Muenchen
+
+A summation operator
+*)
+
+NatSum = Arith +
+consts sum :: "[nat=>nat, nat] => nat"
+rules  sum_0   "sum(f,0) = 0"
+       sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
+end