equal
deleted
inserted
replaced
132 lemma (in monoid_add) sum_list_map_filter: |
132 lemma (in monoid_add) sum_list_map_filter: |
133 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" |
133 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0" |
134 shows "sum_list (map f (filter P xs)) = sum_list (map f xs)" |
134 shows "sum_list (map f (filter P xs)) = sum_list (map f xs)" |
135 using assms by (induct xs) auto |
135 using assms by (induct xs) auto |
136 |
136 |
|
137 lemma sum_list_filter_le_nat: |
|
138 fixes f :: "'a \<Rightarrow> nat" |
|
139 shows "sum_list (map f (filter P xs)) \<le> sum_list (map f xs)" |
|
140 by(induction xs; simp) |
|
141 |
137 lemma (in comm_monoid_add) distinct_sum_list_conv_Sum: |
142 lemma (in comm_monoid_add) distinct_sum_list_conv_Sum: |
138 "distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)" |
143 "distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)" |
139 by (induct xs) simp_all |
144 by (induct xs) simp_all |
140 |
145 |
141 lemma sum_list_upt[simp]: |
146 lemma sum_list_upt[simp]: |
215 by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) |
220 by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) |
216 |
221 |
217 lemma sum_list_mono: |
222 lemma sum_list_mono: |
218 fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" |
223 fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}" |
219 shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)" |
224 shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)" |
220 by (induct xs) (simp, simp add: add_mono) |
225 by (induct xs) (simp, simp add: add_mono) |
|
226 |
|
227 lemma sum_list_strict_mono: |
|
228 fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, strict_ordered_ab_semigroup_add}" |
|
229 shows "\<lbrakk> xs \<noteq> []; \<And>x. x \<in> set xs \<Longrightarrow> f x < g x \<rbrakk> |
|
230 \<Longrightarrow> sum_list (map f xs) < sum_list (map g xs)" |
|
231 proof (induction xs) |
|
232 case Nil thus ?case by simp |
|
233 next |
|
234 case C: (Cons _ xs) |
|
235 show ?case |
|
236 proof (cases xs) |
|
237 case Nil thus ?thesis using C.prems by simp |
|
238 next |
|
239 case Cons thus ?thesis using C by(simp add: add_strict_mono) |
|
240 qed |
|
241 qed |
221 |
242 |
222 lemma (in monoid_add) sum_list_distinct_conv_sum_set: |
243 lemma (in monoid_add) sum_list_distinct_conv_sum_set: |
223 "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)" |
244 "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)" |
224 by (induct xs) simp_all |
245 by (induct xs) simp_all |
225 |
246 |
269 qed |
290 qed |
270 |
291 |
271 lemma sum_list_nonneg: |
292 lemma sum_list_nonneg: |
272 "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0" |
293 "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0" |
273 by (induction xs) simp_all |
294 by (induction xs) simp_all |
|
295 |
|
296 lemma sum_list_Suc: |
|
297 "sum_list (map (\<lambda>x. Suc(f x)) xs) = sum_list (map f xs) + length xs" |
|
298 by(induction xs; simp) |
274 |
299 |
275 lemma (in monoid_add) sum_list_map_filter': |
300 lemma (in monoid_add) sum_list_map_filter': |
276 "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)" |
301 "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)" |
277 by (induction xs) simp_all |
302 by (induction xs) simp_all |
278 |
303 |