1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jul 29 19:47:55 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Jul 30 08:24:46 2011 +0200
     1.3 @@ -397,10 +397,6 @@
     1.4  lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
     1.5  by (metis affine_affine_hull hull_same mem_def)
     1.6  
     1.7 -lemma setsum_restrict_set'': assumes "finite A"
     1.8 -  shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
     1.9 -  unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] ..
    1.10 -
    1.11  subsection {* Some explicit formulations (from Lars Schewe). *}
    1.12  
    1.13  lemma affine: fixes V::"'a::real_vector set"

     2.1 --- a/src/HOL/SetInterval.thy	Fri Jul 29 19:47:55 2011 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Sat Jul 30 08:24:46 2011 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4  
     2.5  context ord
     2.6  begin
     2.7 +
     2.8  definition
     2.9    lessThan    :: "'a => 'a set" ("(1{..<_})") where
    2.10    "{..<u} == {x. x < u}"
    2.11 @@ -1162,12 +1163,18 @@
    2.12            (if m <= n then f m - f(n + 1) else 0)"
    2.13  by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
    2.14  
    2.15 -lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
    2.16 +lemma setsum_restrict_set':
    2.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)"
    2.18 +  by (simp add: setsum_restrict_set [symmetric] Int_def)
    2.19 +
    2.20 +lemma setsum_restrict_set'':
    2.21 +  "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
    2.22 +  by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])
    2.23  
    2.24  lemma setsum_setsum_restrict:
    2.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"
    2.26 -  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
    2.27 -     (rule setsum_commute)
    2.28 +  "finite S \<Longrightarrow> finite T \<Longrightarrow>
    2.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"
    2.30 +  by (simp add: setsum_restrict_set'') (rule setsum_commute)
    2.31  
    2.32  lemma setsum_image_gen: assumes fS: "finite S"
    2.33    shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"