# HG changeset patch
# User paulson
# Date 1091695890 -7200
# Node ID 70d1f5b7d0ad2d3385d91629a70ff17e503dde8b
# Parent  fafcd72b9d4b9fb7bce8811ca1e7cab02007a88b
an updated treatment of the simprules

diff -r fafcd72b9d4b -r 70d1f5b7d0ad src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Thu Aug 05 10:50:58 2004 +0200
+++ b/src/HOL/ex/NatSum.thy	Thu Aug 05 10:51:30 2004 +0200
@@ -17,9 +17,9 @@
   \url{http://www.research.att.com/~njas/sequences/}.
 *}
 
-declare lessThan_Suc [simp] atMost_Suc [simp]
-declare add_mult_distrib [simp] add_mult_distrib2 [simp]
-declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
+lemmas [simp] = lessThan_Suc atMost_Suc  left_distrib right_distrib
+                left_diff_distrib right_diff_distrib --{*for true subtraction*}
+                diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
 
 text {*
   \medskip The sum of the first @{text n} odd numbers equals @{text n}
@@ -97,17 +97,10 @@
   Alternative proof, with a change of variables and much more
   subtraction, performed using the integers. *}
 
-declare
-  zmult_int [symmetric, simp]
-  zadd_zmult_distrib [simp]
-  zadd_zmult_distrib2 [simp]
-  zdiff_zmult_distrib [simp]
-  zdiff_zmult_distrib2 [simp]
-
 lemma int_sum_of_fourth_powers:
-  "30 * int (\<Sum>i \<in> {..<m}. i * i * i * i) =
-    int m * (int m - 1) * (int (2 * m) - 1) *
-    (int (3 * m * m) - int (3 * m) - 1)"
+  "30 * of_nat (\<Sum>i \<in> {..<m}. i * i * i * i) =
+    of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
+    (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
   apply (induct m)
    apply simp_all
   done