src/HOL/Finite_Set.thy
changeset 15554 03d4347b071d
parent 15552 8ab8e425410b
child 15765 6472d4942992
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 01 05:44:13 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 01 18:48:52 2005 +0100
     1.3 @@ -895,8 +895,11 @@
     1.4    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
     1.5  by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
     1.6  
     1.7 +lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
     1.8 +  by (rule setsum_cong[OF refl], auto);
     1.9 +
    1.10  lemma setsum_reindex_cong:
    1.11 -     "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] 
    1.12 +     "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
    1.13        ==> setsum h B = setsum g A"
    1.14    by (simp add: setsum_reindex cong: setsum_cong)
    1.15  
    1.16 @@ -1066,6 +1069,17 @@
    1.17      by (simp add: setsum_def)
    1.18  qed
    1.19  
    1.20 +lemma setsum_strict_mono:
    1.21 +fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
    1.22 +assumes fin_ne: "finite A"  "A \<noteq> {}"
    1.23 +shows "(!!x. x:A \<Longrightarrow> f x < g x) \<Longrightarrow> setsum f A < setsum g A"
    1.24 +using fin_ne
    1.25 +proof (induct rule: finite_ne_induct)
    1.26 +  case singleton thus ?case by simp
    1.27 +next
    1.28 +  case insert thus ?case by (auto simp: add_strict_mono)
    1.29 +qed
    1.30 +
    1.31  lemma setsum_negf:
    1.32   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
    1.33  proof (cases "finite A")