src/HOL/Library/Product_plus.thy
changeset 36627 39b2516a1970
parent 30018 690c65b8ad1a
child 37664 2946b8f057df
     1.1 --- a/src/HOL/Library/Product_plus.thy	Fri Apr 30 13:51:17 2010 -0700
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Sat May 01 07:35:22 2010 -0700
     1.3 @@ -112,4 +112,10 @@
     1.4  instance "*" :: (ab_group_add, ab_group_add) ab_group_add
     1.5    by default (simp_all add: expand_prod_eq)
     1.6  
     1.7 +lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
     1.8 +by (cases "finite A", induct set: finite, simp_all)
     1.9 +
    1.10 +lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
    1.11 +by (cases "finite A", induct set: finite, simp_all)
    1.12 +
    1.13  end