1.1 --- a/src/HOL/Big_Operators.thy	Mon Feb 27 09:01:49 2012 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Mon Feb 27 10:27:21 2012 +0100
     1.3 @@ -523,6 +523,25 @@
     1.4    case insert thus ?case by (auto simp: add_strict_mono)
     1.5  qed
     1.6  
     1.7 +lemma setsum_strict_mono_ex1:
     1.8 +fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
     1.9 +assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
    1.10 +shows "setsum f A < setsum g A"
    1.11 +proof-
    1.12 +  from assms(3) obtain a where a: "a:A" "f a < g a" by blast
    1.13 +  have "setsum f A = setsum f ((A-{a}) \<union> {a})"
    1.14 +    by(simp add:insert_absorb[OF `a:A`])
    1.15 +  also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
    1.16 +    using `finite A` by(subst setsum_Un_disjoint) auto
    1.17 +  also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
    1.18 +    by(rule setsum_mono)(simp add: assms(2))
    1.19 +  also have "setsum f {a} < setsum g {a}" using a by simp
    1.20 +  also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
    1.21 +    using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
    1.22 +  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
    1.23 +  finally show ?thesis by (metis add_right_mono add_strict_left_mono)
    1.24 +qed
    1.25 +
    1.26  lemma setsum_negf:
    1.27    "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
    1.28  proof (cases "finite A")