# HG changeset patch
# User paulson
# Date 957802804 -7200
# Node ID 9ee87bdcba056a53b05f58e16ccac87ad222a318
# Parent  32fe62227ff097e898ea832f445fa1237af697f8
yet another example

diff -r 32fe62227ff0 -r 9ee87bdcba05 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Mon May 08 16:59:18 2000 +0200
+++ b/src/HOL/ex/NatSum.ML	Mon May 08 18:20:04 2000 +0200
@@ -60,4 +60,17 @@
 by (Simp_tac 1);
 qed "sum_of_fourth_powers";
 
+(** Alternative proof, avoiding the need for inequality reasoning **)
 
+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);
+qed "int_sum_of_fourth_powers";
+
+