author nipkow Sun Nov 04 09:57:49 2018 +0100 (6 months ago) changeset 69231 6b90ace5e5eb parent 69230 07fc77bf5eb6 child 69232 2b913054a9cf
more lemmas
 src/HOL/Groups_List.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Groups_List.thy	Sat Nov 03 20:30:10 2018 +0100
1.2 +++ b/src/HOL/Groups_List.thy	Sun Nov 04 09:57:49 2018 +0100
1.3 @@ -134,6 +134,11 @@
1.4    shows "sum_list (map f (filter P xs)) = sum_list (map f xs)"
1.5    using assms by (induct xs) auto
1.6
1.7 +lemma sum_list_filter_le_nat:
1.8 +  fixes f :: "'a \<Rightarrow> nat"
1.9 +  shows "sum_list (map f (filter P xs)) \<le> sum_list (map f xs)"
1.10 +by(induction xs; simp)
1.11 +
1.12  lemma (in comm_monoid_add) distinct_sum_list_conv_Sum:
1.13    "distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)"
1.14    by (induct xs) simp_all
1.15 @@ -217,7 +222,23 @@
1.16  lemma sum_list_mono:
1.17    fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
1.18    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)"
1.19 -  by (induct xs) (simp, simp add: add_mono)
1.20 +by (induct xs) (simp, simp add: add_mono)
1.21 +
1.22 +lemma sum_list_strict_mono:
1.23 +  fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, strict_ordered_ab_semigroup_add}"
1.24 +  shows "\<lbrakk> xs \<noteq> [];  \<And>x. x \<in> set xs \<Longrightarrow> f x < g x \<rbrakk>
1.25 +    \<Longrightarrow> sum_list (map f xs) < sum_list (map g xs)"
1.26 +proof (induction xs)
1.27 +  case Nil thus ?case by simp
1.28 +next
1.29 +  case C: (Cons _ xs)
1.30 +  show ?case
1.31 +  proof (cases xs)
1.32 +    case Nil thus ?thesis using C.prems by simp
1.33 +  next
1.34 +    case Cons thus ?thesis using C by(simp add: add_strict_mono)
1.35 +  qed
1.36 +qed
1.37
1.38  lemma (in monoid_add) sum_list_distinct_conv_sum_set:
1.39    "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)"
1.40 @@ -272,6 +293,10 @@
1.41      "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
1.42    by (induction xs) simp_all
1.43
1.44 +lemma sum_list_Suc:
1.45 +  "sum_list (map (\<lambda>x. Suc(f x)) xs) = sum_list (map f xs) + length xs"
1.46 +by(induction xs; simp)
1.47 +
1.48  lemma (in monoid_add) sum_list_map_filter':
1.49    "sum_list (map f (filter P xs)) = sum_list (map (\<lambda>x. if P x then f x else 0) xs)"
1.50    by (induction xs) simp_all
```