src/HOL/Groups_List.thy
changeset 69231 6b90ace5e5eb
parent 69064 5840724b1d71
child 69593 3dda49e08b9d
     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