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