Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
authorobua
Tue Nov 23 15:25:39 2004 +0100 (2004-11-23)
changeset 153112ca1c66a6758
parent 15310 7a5ded09f68b
child 15312 7d6e12ead964
Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Nov 23 14:21:24 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 23 15:25:39 2004 +0100
     1.3 @@ -999,6 +999,50 @@
     1.4    thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
     1.5  qed
     1.6  
     1.7 +lemma setsum_mono:
     1.8 +  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
     1.9 +  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
    1.10 +proof (cases "finite K")
    1.11 +  case True
    1.12 +  thus ?thesis using le
    1.13 +  proof (induct)
    1.14 +    case empty
    1.15 +    thus ?case by simp
    1.16 +  next
    1.17 +    case insert
    1.18 +    thus ?case using add_mono 
    1.19 +      by force
    1.20 +  qed
    1.21 +next
    1.22 +  case False
    1.23 +  thus ?thesis
    1.24 +    by (simp add: setsum_def)
    1.25 +qed
    1.26 +
    1.27 +lemma finite_setsum_diff1: "finite A \<Longrightarrow> (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) =
    1.28 +    (if a:A then setsum f A - f a else setsum f A)"
    1.29 +  by (erule finite_induct) (auto simp add: insert_Diff_if)
    1.30 +
    1.31 +lemma finite_setsum_diff:
    1.32 +  assumes le: "finite A" "B \<subseteq> A"
    1.33 +  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))"
    1.34 +proof -
    1.35 +  from le have finiteB: "finite B" using finite_subset by auto
    1.36 +  show ?thesis using le finiteB
    1.37 +    proof (induct rule: Finites.induct[OF finiteB])
    1.38 +      case 1
    1.39 +      thus ?case by auto
    1.40 +    next
    1.41 +      case 2
    1.42 +      thus ?case using le 
    1.43 +	apply auto
    1.44 +	apply (subst Diff_insert)
    1.45 +	apply (subst finite_setsum_diff1)
    1.46 +	apply (auto simp add: insert_absorb)
    1.47 +	done
    1.48 +    qed
    1.49 +  qed
    1.50 +
    1.51  lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::comm_ring_1) A =
    1.52    - setsum f A"
    1.53    by (induct set: Finites, auto)