1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 01 09:31:10 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 01 19:53:30 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/Predicate.thy	Mon Aug 01 09:31:10 2011 -0700
     2.2 +++ b/src/HOL/Predicate.thy	Mon Aug 01 19:53:30 2011 +0200
     2.3 @@ -741,11 +741,12 @@
     2.4  by simp
     2.5  
     2.6  lemma closure_of_bool_cases [no_atp]:
     2.7 -assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
     2.8 -assumes "f = (%u. True) \<Longrightarrow> P f"
     2.9 -shows "P f"
    2.10 +  fixes f :: "unit \<Rightarrow> bool"
    2.11 +  assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
    2.12 +  assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
    2.13 +  shows "P f"
    2.14  proof -
    2.15 -  have "f = (%u. False) \<or> f = (%u. True)"
    2.16 +  have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
    2.17      apply (cases "f ()")
    2.18      apply (rule disjI2)
    2.19      apply (rule ext)
    2.20 @@ -758,19 +759,18 @@
    2.21  qed
    2.22  
    2.23  lemma unit_pred_cases:
    2.24 -assumes "P \<bottom>"
    2.25 -assumes "P (single ())"
    2.26 -shows "P Q"
    2.27 -using assms
    2.28 -unfolding bot_pred_def Collect_def empty_def single_def
    2.29 -apply (cases Q)
    2.30 -apply simp
    2.31 -apply (rule_tac f="fun" in closure_of_bool_cases)
    2.32 -apply auto
    2.33 -apply (subgoal_tac "(%x. () = x) = (%x. True)") 
    2.34 -apply auto
    2.35 -done
    2.36 -
    2.37 +  assumes "P \<bottom>"
    2.38 +  assumes "P (single ())"
    2.39 +  shows "P Q"
    2.40 +using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
    2.41 +  fix f
    2.42 +  assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
    2.43 +  then have "P (Pred f)" 
    2.44 +    by (cases _ f rule: closure_of_bool_cases) simp_all
    2.45 +  moreover assume "Q = Pred f"
    2.46 +  ultimately show "P Q" by simp
    2.47 +qed
    2.48 +  
    2.49  lemma holds_if_pred:
    2.50    "holds (if_pred b) = b"
    2.51  unfolding if_pred_eq holds_eq

     3.1 --- a/src/HOL/SetInterval.thy	Mon Aug 01 09:31:10 2011 -0700
     3.2 +++ b/src/HOL/SetInterval.thy	Mon Aug 01 19:53:30 2011 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4  
     3.5  context ord
     3.6  begin
     3.7 +
     3.8  definition
     3.9    lessThan    :: "'a => 'a set" ("(1{..<_})") where
    3.10    "{..<u} == {x. x < u}"
    3.11 @@ -1162,12 +1163,18 @@
    3.12            (if m <= n then f m - f(n + 1) else 0)"
    3.13  by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
    3.14  
    3.15 -lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
    3.16 +lemma setsum_restrict_set':
    3.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)"
    3.18 +  by (simp add: setsum_restrict_set [symmetric] Int_def)
    3.19 +
    3.20 +lemma setsum_restrict_set'':
    3.21 +  "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
    3.22 +  by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])
    3.23  
    3.24  lemma setsum_setsum_restrict:
    3.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"
    3.26 -  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
    3.27 -     (rule setsum_commute)
    3.28 +  "finite S \<Longrightarrow> finite T \<Longrightarrow>
    3.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"
    3.30 +  by (simp add: setsum_restrict_set'') (rule setsum_commute)
    3.31  
    3.32  lemma setsum_image_gen: assumes fS: "finite S"
    3.33    shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"