# HG changeset patch
# User paulson
# Date 957797958 -7200
# Node ID 32fe62227ff097e898ea832f445fa1237af697f8
# Parent  56187238220d69364f176bc706f22c3898c585e6
new example

diff -r 56187238220d -r 32fe62227ff0 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Mon May 08 16:59:02 2000 +0200
+++ b/src/HOL/ex/NatSum.ML	Mon May 08 16:59:18 2000 +0200
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
-Summing natural numbers, squares and cubes.  Could be continued...
+Summing natural numbers, squares, cubes, etc.
 
 Originally demonstrated permutative rewriting, but add_ac is no longer needed
   thanks to new simprocs.
@@ -32,3 +32,32 @@
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_cubes";
+
+(** Sum of fourth powers requires lemmas **)
+
+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);
+qed "sum_of_fourth_powers";
+
+
diff -r 56187238220d -r 32fe62227ff0 src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Mon May 08 16:59:02 2000 +0200
+++ b/src/HOL/ex/NatSum.thy	Mon May 08 16:59:18 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/natsum.thy
+(*  Title:      HOL/ex/NatSum.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
@@ -9,7 +9,7 @@
 NatSum = Main +
 consts sum     :: [nat=>nat, nat] => nat
 primrec 
-  "sum f 0 = 0"
-  "sum f (Suc n) = f(n) + sum f n"
+  sum_0    "sum f 0 = 0"
+  sum_Suc  "sum f (Suc n) = f(n) + sum f n"
 
 end