# HG changeset patch
# User paulson
# Date 959260844 -7200
# Node ID 340d306f0118277781063d4ba951a9f88394ad61
# Parent  bcd34d580839e6c093e31707902a40519a21b2c0
setsum replaces sum_below

diff -r bcd34d580839 -r 340d306f0118 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Thu May 25 15:15:54 2000 +0200
+++ b/src/HOL/ex/NatSum.ML	Thu May 25 15:20:44 2000 +0200
@@ -12,17 +12,18 @@
   http://www.research.att.com/~njas/sequences/
 *)
 
+Addsimps [lessThan_Suc, atMost_Suc];
 Addsimps [add_mult_distrib, add_mult_distrib2];
 Addsimps [diff_mult_distrib, diff_mult_distrib2];
 
 (*The sum of the first n odd numbers equals n squared.*)
-Goal "sum_below (%i. Suc(i+i)) n = n*n";
+Goal "setsum (%i. Suc(i+i)) (lessThan n) = n*n";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_odds";
 
 (*The sum of the first n odd squares*)
-Goal "#3 * sum_below (%i. Suc(i+i)*Suc(i+i)) n = n * (#4*n*n - #1)";
+Goal "#3 * setsum (%i. Suc(i+i)*Suc(i+i)) (lessThan n) = n * (#4*n*n - #1)";
 by (induct_tac "n" 1);
 (*This removes the -#1 from the inductive step*)
 by (case_tac "n" 2);
@@ -30,7 +31,7 @@
 qed "sum_of_odd_squares";
 
 (*The sum of the first n odd cubes*)
-Goal "sum_below (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) n = n * n * (#2*n*n - #1)";
+Goal "setsum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) (lessThan n) = n * n * (#2*n*n - #1)";
 by (induct_tac "n" 1);
 (*This removes the -#1 from the inductive step*)
 by (case_tac "n" 2);
@@ -38,44 +39,39 @@
 qed "sum_of_odd_cubes";
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
-Goal "#2 * sum_below id (Suc n) = n*Suc(n)";
+Goal "#2 * setsum id (atMost n) = n*Suc(n)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_naturals";
 
-Goal "#6 * sum_below (%i. i*i) (Suc n) = n * Suc(n) * Suc(#2*n)";
+Goal "#6 * setsum (%i. i*i) (atMost n) = n * Suc(n) * Suc(#2*n)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_squares";
 
-Goal "#4 * sum_below (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)";
+Goal "#4 * setsum (%i. i*i*i) (atMost n) = n * n * Suc(n) * Suc(n)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_cubes";
 
 (** Sum of fourth powers: two versions **)
 
-Goal "#30 * sum_below (%i. i*i*i*i) (Suc n) = \
+Goal "#30 * setsum (%i. i*i*i*i) (atMost n) = \
 \     n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)";
 by (induct_tac "n" 1);
-by (Simp_tac 1);
-(*In simplifying we want only the outer Suc argument to be unfolded.
-  Thus the result matches the induction hypothesis (also with Suc). *)
-by (asm_simp_tac (simpset() delsimps [sum_below_Suc]
-                            addsimps [inst "n" "Suc ?m" sum_below_Suc]) 1);
+by Auto_tac;
 (*Eliminates the subtraction*)
 by (case_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "sum_of_fourth_powers";
 
-(*Alternative proof.  The change of variables n |-> m-#1 eliminates the tricky
-  rewriting of Suc (Suc n).  Because it involves much more subtraction, we
-  switch to the integers. *)
+(*Alternative proof, with a change of variables and much more subtraction, 
+  performed using the integers.*)
 
 Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, 
 	  zdiff_zmult_distrib, zdiff_zmult_distrib2];
 
-Goal "#30 * int (sum_below (%i. i*i*i*i) m) = \
+Goal "#30 * int (setsum (%i. i*i*i*i) (lessThan m)) = \
 \         int m * (int m - #1) * (int (#2*m) - #1) * \
 \         (int (#3*m*m) - int(#3*m) - #1)";
 by (induct_tac "m" 1);
@@ -84,17 +80,17 @@
 
 (** Sums of geometric series: 2, 3 and the general case **)
 
-Goal "sum_below (%i. #2^i) n = #2^n - 1";
+Goal "setsum (%i. #2^i) (lessThan n) = #2^n - 1";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_2_powers";
 
-Goal "#2 * sum_below (%i. #3^i) n = #3^n - 1";
+Goal "#2 * setsum (%i. #3^i) (lessThan n) = #3^n - 1";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_3_powers";
 
-Goal "0<k ==> (k-1) * sum_below (%i. k^i) n = k^n - 1";
+Goal "0<k ==> (k-1) * setsum (%i. k^i) (lessThan n) = k^n - 1";
 by (induct_tac "n" 1);
 by Auto_tac;
 by (subgoal_tac "1*k^n <= k * k^n" 1);