# HG changeset patch
# User paulson
# Date 957864553 -7200
# Node ID b90d653bd089b9fe9f6cca628a953649aabdd663
# Parent  95f2b61f238939212d1f55d34fcc51d56df04f4c
more examples

diff -r 95f2b61f2389 -r b90d653bd089 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Mon May 08 21:00:27 2000 +0200
+++ b/src/HOL/ex/NatSum.ML	Tue May 09 11:29:13 2000 +0200
@@ -7,15 +7,34 @@
 
 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 [add_mult_distrib, add_mult_distrib2];
+
 (*The sum of the first n odd numbers equals n squared.*)
 Goal "sum (%i. Suc(i+i)) n = n*n";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_odds";
 
-Addsimps [add_mult_distrib, add_mult_distrib2];
+(*The sum of the first n odd squares*)
+Goal "#3 * sum (%i. Suc(i+i)*Suc(i+i)) n = n * (#4*n*n - #1)";
+by (induct_tac "n" 1);
+(*This removes the -#1 from the inductive step*)
+by (case_tac "n" 2);
+by Auto_tac;
+qed "sum_of_odd_squares";
+
+(*The sum of the first n odd cubes*)
+Goal "sum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) 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);
+by Auto_tac;
+qed "sum_of_odd_cubes";
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
 Goal "#2 * sum id (Suc n) = n*Suc(n)";
@@ -33,44 +52,31 @@
 by Auto_tac;
 qed "sum_of_cubes";
 
-(** Sum of fourth powers requires lemmas **)
+(** Sum of fourth powers: two versions **)
 
-Goal "[| #1 <= (j::nat); k <= m |] ==> k <= j*m";
-by (dtac mult_le_mono 1);
-by Auto_tac;
-qed "mult_le_1_mono";
-
-Addsimps [diff_mult_distrib, diff_mult_distrib2];
-
-(*Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
-  http://www.research.att.com/~njas/sequences/*)
 Goal "#30 * sum (%i. i*i*i*i) (Suc n) = \
 \     n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)";
 by (induct_tac "n" 1);
 by (Simp_tac 1);
-(*Automating this inequality proof would make the proof trivial*)
-by (subgoal_tac "n <= #10 * (n * (n * n)) + (#15 * (n * (n * (n * n))) + \
-\                     #6 * (n * (n * (n * (n * n)))))" 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_Suc]
                             addsimps [inst "n" "Suc ?m" sum_Suc]) 1);
-by (rtac ([mult_le_1_mono, le_add1] MRS le_trans) 1);
-by (rtac le_cube 2);
-by (Simp_tac 1);
+(*Eliminates the subtraction*)
+by (case_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "sum_of_fourth_powers";
 
-(** Alternative proof, avoiding the need for inequality reasoning **)
+(*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. *)
 
 Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, 
 	  zdiff_zmult_distrib, zdiff_zmult_distrib2];
 
-Goal "#30 * int (sum (%i. i*i*i*i) (Suc n)) = \
-\     int n * int(Suc n) * int (Suc(#2*n)) * (int (#3*n*n) + int (#3*n) - #1)";
-by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() delsimps [sum_Suc]
-                            addsimps [inst "n" "Suc ?m" sum_Suc]) 1);
+Goal "#30 * int (sum (%i. i*i*i*i) m) = \
+\         int m * (int m - #1) * (int (#2*m) - #1) * \
+\         (int (#3*m*m) - int(#3*m) - #1)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "int_sum_of_fourth_powers";
-
-