author paulson Thu Aug 05 10:51:30 2004 +0200 (2004-08-05) changeset 15114 70d1f5b7d0ad parent 15113 fafcd72b9d4b child 15115 1c3be9eb4126
an updated treatment of the simprules
 src/HOL/ex/NatSum.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/ex/NatSum.thy	Thu Aug 05 10:50:58 2004 +0200
1.2 +++ b/src/HOL/ex/NatSum.thy	Thu Aug 05 10:51:30 2004 +0200
1.3 @@ -17,9 +17,9 @@
1.4    \url{http://www.research.att.com/~njas/sequences/}.
1.5  *}
1.6
1.7 -declare lessThan_Suc [simp] atMost_Suc [simp]
1.9 -declare diff_mult_distrib [simp] diff_mult_distrib2 [simp]
1.10 +lemmas [simp] = lessThan_Suc atMost_Suc  left_distrib right_distrib
1.11 +                left_diff_distrib right_diff_distrib --{*for true subtraction*}
1.12 +                diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
1.13
1.14  text {*
1.15    \medskip The sum of the first @{text n} odd numbers equals @{text n}
1.16 @@ -97,17 +97,10 @@
1.17    Alternative proof, with a change of variables and much more
1.18    subtraction, performed using the integers. *}
1.19
1.20 -declare
1.21 -  zmult_int [symmetric, simp]
1.24 -  zdiff_zmult_distrib [simp]
1.25 -  zdiff_zmult_distrib2 [simp]
1.26 -
1.27  lemma int_sum_of_fourth_powers:
1.28 -  "30 * int (\<Sum>i \<in> {..<m}. i * i * i * i) =
1.29 -    int m * (int m - 1) * (int (2 * m) - 1) *
1.30 -    (int (3 * m * m) - int (3 * m) - 1)"
1.31 +  "30 * of_nat (\<Sum>i \<in> {..<m}. i * i * i * i) =
1.32 +    of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
1.33 +    (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
1.34    apply (induct m)
1.35     apply simp_all
1.36    done
```