src/HOL/SetInterval.thy
changeset 44879 2e09299ce807
parent 44515 537ea3846f64
child 45761 22f665a2e91c
     1.1 --- a/src/HOL/SetInterval.thy	Fri Jul 29 19:47:55 2011 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Sat Jul 30 08:24:46 2011 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  
     1.5  context ord
     1.6  begin
     1.7 +
     1.8  definition
     1.9    lessThan    :: "'a => 'a set" ("(1{..<_})") where
    1.10    "{..<u} == {x. x < u}"
    1.11 @@ -1162,12 +1163,18 @@
    1.12            (if m <= n then f m - f(n + 1) else 0)"
    1.13  by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
    1.14  
    1.15 -lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
    1.16 +lemma setsum_restrict_set':
    1.17 +  "finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)"
    1.18 +  by (simp add: setsum_restrict_set [symmetric] Int_def)
    1.19 +
    1.20 +lemma setsum_restrict_set'':
    1.21 +  "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
    1.22 +  by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])
    1.23  
    1.24  lemma setsum_setsum_restrict:
    1.25 -  "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.26 -  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
    1.27 -     (rule setsum_commute)
    1.28 +  "finite S \<Longrightarrow> finite T \<Longrightarrow>
    1.29 +    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.30 +  by (simp add: setsum_restrict_set'') (rule setsum_commute)
    1.31  
    1.32  lemma setsum_image_gen: assumes fS: "finite S"
    1.33    shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"