generalize setsum lemmas from semiring_0_cancel to semiring_0
authorhuffman
Fri May 11 03:31:12 2007 +0200 (2007-05-11)
changeset 2293464ecb3d6790a
parent 22933 338c7890c96f
child 22935 c6689e15bc98
generalize setsum lemmas from semiring_0_cancel to semiring_0
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri May 11 01:07:10 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri May 11 03:31:12 2007 +0200
     1.3 @@ -1148,7 +1148,7 @@
     1.4  done
     1.5  
     1.6  lemma setsum_right_distrib: 
     1.7 -  fixes f :: "'a => ('b::semiring_0_cancel)"
     1.8 +  fixes f :: "'a => ('b::semiring_0)"
     1.9    shows "r * setsum f A = setsum (%n. r * f n) A"
    1.10  proof (cases "finite A")
    1.11    case True
    1.12 @@ -1163,7 +1163,7 @@
    1.13  qed
    1.14  
    1.15  lemma setsum_left_distrib:
    1.16 -  "setsum f A * (r::'a::semiring_0_cancel) = (\<Sum>n\<in>A. f n * r)"
    1.17 +  "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
    1.18  proof (cases "finite A")
    1.19    case True
    1.20    then show ?thesis
    1.21 @@ -1270,7 +1270,7 @@
    1.22  qed
    1.23  
    1.24  lemma setsum_product:
    1.25 -  fixes f :: "'a => ('b::semiring_0_cancel)"
    1.26 +  fixes f :: "'a => ('b::semiring_0)"
    1.27    shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
    1.28    by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
    1.29