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)"