1.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 17 09:22:40 2010 -0800
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 17 17:57:37 2010 +0100
     1.3 @@ -2034,6 +2034,31 @@
     1.4    apply auto
     1.5  done
     1.6  
     1.7 +lemma setprod_mono:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
     1.9 +  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
    1.10 +  shows "setprod f A \<le> setprod g A"
    1.11 +proof (cases "finite A")
    1.12 +  case True
    1.13 +  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
    1.14 +  proof (induct A rule: finite_subset_induct)
    1.15 +    case (insert a F)
    1.16 +    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
    1.17 +      unfolding setprod_insert[OF insert(1,3)]
    1.18 +      using assms[rule_format,OF insert(2)] insert
    1.19 +      by (auto intro: mult_mono mult_nonneg_nonneg)
    1.20 +  qed auto
    1.21 +  thus ?thesis by simp
    1.22 +qed auto
    1.23 +
    1.24 +lemma abs_setprod:
    1.25 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
    1.26 +  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
    1.27 +proof (cases "finite A")
    1.28 +  case True thus ?thesis
    1.29 +    by induct (auto simp add: field_simps setprod_insert abs_mult)
    1.30 +qed auto
    1.31 +
    1.32  
    1.33  subsection {* Finite cardinality *}
    1.34  

     2.1 --- a/src/HOL/SetInterval.thy	Wed Feb 17 09:22:40 2010 -0800
     2.2 +++ b/src/HOL/SetInterval.thy	Wed Feb 17 17:57:37 2010 +0100
     2.3 @@ -970,6 +970,27 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma setsum_le_included:
     2.8 +  fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}"
     2.9 +  assumes "finite s" "finite t"
    2.10 +  and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
    2.11 +  shows "setsum f s \<le> setsum g t"
    2.12 +proof -
    2.13 +  have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
    2.14 +  proof (rule setsum_mono)
    2.15 +    fix y assume "y \<in> s"
    2.16 +    with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
    2.17 +    with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
    2.18 +      using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
    2.19 +      by (auto intro!: setsum_mono2)
    2.20 +  qed
    2.21 +  also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
    2.22 +    using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
    2.23 +  also have "... \<le> setsum g t"
    2.24 +    using assms by (auto simp: setsum_image_gen[symmetric])
    2.25 +  finally show ?thesis .
    2.26 +qed
    2.27 +
    2.28  lemma setsum_multicount_gen:
    2.29    assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
    2.30    shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")