# HG changeset patch
# User paulson
# Date 966594680 -7200
# Node ID e9623f47275b76211d791dea58043b21650ce2c5
# Parent  aa3b82085e072b5f4f565e993d1b2c37afbad817
new example ZF/ex/NatSum

diff -r aa3b82085e07 -r e9623f47275b NEWS
--- a/NEWS	Fri Aug 18 12:30:41 2000 +0200
+++ b/NEWS	Fri Aug 18 12:31:20 2000 +0200
@@ -303,6 +303,7 @@
 * the integer library now contains many of the usual laws for the orderings, 
 including $<=, and monotonicity laws for $+ and $*; 
 
+* new example ZF/ex/NatSum to demonstrate integer arithmetic simplification;
 
 *** FOL & ZF ***
 
diff -r aa3b82085e07 -r e9623f47275b src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Fri Aug 18 12:30:41 2000 +0200
+++ b/src/ZF/IsaMakefile	Fri Aug 18 12:31:20 2000 +0200
@@ -114,7 +114,7 @@
   ex/Enum.thy ex/LList.ML ex/LList.thy \
   ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
   ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
-  ex/Primrec_defs.ML ex/Primrec_defs.thy \
+  ex/NatSum.ML ex/NatSum.thy  ex/Primrec_defs.ML ex/Primrec_defs.thy \
   ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
   ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
   ex/Term.ML ex/Term.thy ex/misc.ML
diff -r aa3b82085e07 -r e9623f47275b src/ZF/ex/NatSum.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/NatSum.ML	Fri Aug 18 12:31:20 2000 +0200
@@ -0,0 +1,64 @@
+(*  Title:      HOL/ex/NatSum.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow & Lawrence C Paulson
+
+Summing natural numbers, squares, cubes, etc.
+
+Originally demonstrated permutative rewriting, but add_ac is no longer needed
+  thanks to new simprocs.
+
+Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
+  http://www.research.att.com/~njas/sequences/
+*)
+
+Addsimps [zadd_zmult_distrib, zadd_zmult_distrib2];
+Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2];
+
+(*The sum of the first n odd numbers equals n squared.*)
+Goal "n: nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sum_of_odds";
+
+(*The sum of the first n odd squares*)
+Goal "n: nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
+\     $#n $* (#4 $* $#n $* $#n $- #1)";
+by (induct_tac "n" 1);
+by Auto_tac;  
+qed "sum_of_odd_squares";
+
+(*The sum of the first n odd cubes*)
+Goal "n: nat \
+\     ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
+\         $#n $* $#n $* (#2 $* $#n $* $#n $- #1)";
+by (induct_tac "n" 1);
+by Auto_tac;  
+qed "sum_of_odd_cubes";
+
+(*The sum of the first n positive integers equals n(n+1)/2.*)
+Goal "n: nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sum_of_naturals";
+
+Goal "n: nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
+\                $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sum_of_squares";
+
+Goal "n: nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
+\                $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sum_of_cubes";
+
+(** Sum of fourth powers **)
+
+Goal "n: nat ==> \
+\     #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \
+\     $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \
+\     (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sum_of_fourth_powers";
diff -r aa3b82085e07 -r e9623f47275b src/ZF/ex/NatSum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/NatSum.thy	Fri Aug 18 12:31:20 2000 +0200
@@ -0,0 +1,18 @@
+(*  Title:      HOL/ex/Natsum.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Lawrence C Paulson
+
+A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
+
+Note: n is a natural number but the sum is an integer,
+                            and f maps integers to integers
+*)
+
+NatSum = Main +
+
+consts sum     :: [i=>i, i] => i
+primrec 
+  "sum (f,0) = #0"
+  "sum (f, succ(n)) = f($#n) $+ sum(f,n)"
+
+end
\ No newline at end of file
diff -r aa3b82085e07 -r e9623f47275b src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Fri Aug 18 12:30:41 2000 +0200
+++ b/src/ZF/ex/ROOT.ML	Fri Aug 18 12:31:20 2000 +0200
@@ -8,6 +8,7 @@
 
 time_use     "misc.ML";
 time_use_thy "Primes";          (*GCD theory*)
+time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
 time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
 time_use_thy "Limit";           (*Inverse limit construction of domains*)
 time_use     "BinEx";		(*Binary integer arithmetic*)