an updated treatment of the simprules
authorpaulson
Thu Aug 05 10:51:30 2004 +0200 (2004-08-05)
changeset 1511470d1f5b7d0ad
parent 15113 fafcd72b9d4b
child 15115 1c3be9eb4126
an updated treatment of the simprules
src/HOL/ex/NatSum.thy
     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.8 -declare add_mult_distrib [simp] add_mult_distrib2 [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.22 -  zadd_zmult_distrib [simp]
    1.23 -  zadd_zmult_distrib2 [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