equal
deleted
inserted
replaced
3203 apply arith |
3203 apply arith |
3204 done |
3204 done |
3205 |
3205 |
3206 lemma (in monoid_add) listsum_triv: |
3206 lemma (in monoid_add) listsum_triv: |
3207 "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" |
3207 "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" |
3208 by (induct xs) (simp_all add: left_distrib) |
3208 by (induct xs) (simp_all add: distrib_right) |
3209 |
3209 |
3210 lemma (in monoid_add) listsum_0 [simp]: |
3210 lemma (in monoid_add) listsum_0 [simp]: |
3211 "(\<Sum>x\<leftarrow>xs. 0) = 0" |
3211 "(\<Sum>x\<leftarrow>xs. 0) = 0" |
3212 by (induct xs) (simp_all add: left_distrib) |
3212 by (induct xs) (simp_all add: distrib_right) |
3213 |
3213 |
3214 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} |
3214 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} |
3215 lemma (in ab_group_add) uminus_listsum_map: |
3215 lemma (in ab_group_add) uminus_listsum_map: |
3216 "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)" |
3216 "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)" |
3217 by (induct xs) simp_all |
3217 by (induct xs) simp_all |