author huffman Tue, 26 May 2009 10:31:39 -0700 changeset 31258 43a418a41317 parent 31257 547bf9819d6c child 31259 c1b981b71dba
listsum lemmas
 src/HOL/List.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/List.thy	Tue May 26 07:39:52 2009 -0700
+++ b/src/HOL/List.thy	Tue May 26 10:31:39 2009 -0700
@@ -2212,6 +2212,36 @@
shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
by (induct xs) simp_all

+  fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
+  shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
+by (induct xs) (simp_all add: algebra_simps)
+
+lemma listsum_subtractf:
+  fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
+  shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
+by (induct xs) simp_all
+
+lemma listsum_const_mult:
+  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+  shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
+by (induct xs, simp_all add: algebra_simps)
+
+lemma listsum_mult_const:
+  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
+  shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
+by (induct xs, simp_all add: algebra_simps)
+
+lemma listsum_abs:
+  fixes xs :: "'a::pordered_ab_group_add_abs list"
+  shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
+by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
+
+lemma listsum_mono: