more lemmas
authornipkow
Mon Jun 08 20:43:57 2009 +0200 (2009-06-08)
changeset 3150900ede188c5d6
parent 31508 1ea1c70aba00
child 31510 e0f2bb4b0021
child 31520 0a99c8716312
more lemmas
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Mon Jun 08 18:34:02 2009 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Jun 08 20:43:57 2009 +0200
     1.3 @@ -859,6 +859,43 @@
     1.4            (if m <= n then f m - f(n + 1) else 0)"
     1.5  by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
     1.6  
     1.7 +lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
     1.8 +
     1.9 +lemma setsum_setsum_restrict:
    1.10 +  "finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
    1.11 +  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
    1.12 +     (rule setsum_commute)
    1.13 +
    1.14 +lemma setsum_image_gen: assumes fS: "finite S"
    1.15 +  shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
    1.16 +proof-
    1.17 +  { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto }
    1.18 +  hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
    1.19 +    by simp
    1.20 +  also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
    1.21 +    by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])
    1.22 +  finally show ?thesis .
    1.23 +qed
    1.24 +
    1.25 +lemma setsum_multicount_gen:
    1.26 +  assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
    1.27 +  shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
    1.28 +proof-
    1.29 +  have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
    1.30 +  also have "\<dots> = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]
    1.31 +    using assms(3) by auto
    1.32 +  finally show ?thesis .
    1.33 +qed
    1.34 +
    1.35 +lemma setsum_multicount:
    1.36 +  assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
    1.37 +  shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
    1.38 +proof-
    1.39 +  have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
    1.40 +  also have "\<dots> = ?r" by(simp add: setsum_constant mult_commute)
    1.41 +  finally show ?thesis by auto
    1.42 +qed
    1.43 +
    1.44  
    1.45  subsection{* Shifting bounds *}
    1.46