# HG changeset patch
# User haftmann
# Date 1312221210 -7200
# Node ID 9be0f4a6f155018e762d26f7279a97055f1d84b6
# Parent  b9839fad3bb62682f4cf8d7fde8a68b65c35f1f0# Parent  2e09299ce807d659114b00b5808236f45e292f03
merged

diff -r b9839fad3bb6 -r 9be0f4a6f155 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 01 09:31:10 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 01 19:53:30 2011 +0200
@@ -397,10 +397,6 @@
 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
 by (metis affine_affine_hull hull_same mem_def)
 
-lemma setsum_restrict_set'': assumes "finite A"
-  shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
-  unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] ..
-
 subsection {* Some explicit formulations (from Lars Schewe). *}
 
 lemma affine: fixes V::"'a::real_vector set"
diff -r b9839fad3bb6 -r 9be0f4a6f155 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Aug 01 09:31:10 2011 -0700
+++ b/src/HOL/Predicate.thy	Mon Aug 01 19:53:30 2011 +0200
@@ -741,11 +741,12 @@
 by simp
 
 lemma closure_of_bool_cases [no_atp]:
-assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
-assumes "f = (%u. True) \<Longrightarrow> P f"
-shows "P f"
+  fixes f :: "unit \<Rightarrow> bool"
+  assumes "f = (\<lambda>u. False) \<Longrightarrow> P f"
+  assumes "f = (\<lambda>u. True) \<Longrightarrow> P f"
+  shows "P f"
 proof -
-  have "f = (%u. False) \<or> f = (%u. True)"
+  have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)"
     apply (cases "f ()")
     apply (rule disjI2)
     apply (rule ext)
@@ -758,19 +759,18 @@
 qed
 
 lemma unit_pred_cases:
-assumes "P \<bottom>"
-assumes "P (single ())"
-shows "P Q"
-using assms
-unfolding bot_pred_def Collect_def empty_def single_def
-apply (cases Q)
-apply simp
-apply (rule_tac f="fun" in closure_of_bool_cases)
-apply auto
-apply (subgoal_tac "(%x. () = x) = (%x. True)") 
-apply auto
-done
-
+  assumes "P \<bottom>"
+  assumes "P (single ())"
+  shows "P Q"
+using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
+  fix f
+  assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
+  then have "P (Pred f)" 
+    by (cases _ f rule: closure_of_bool_cases) simp_all
+  moreover assume "Q = Pred f"
+  ultimately show "P Q" by simp
+qed
+  
 lemma holds_if_pred:
   "holds (if_pred b) = b"
 unfolding if_pred_eq holds_eq
diff -r b9839fad3bb6 -r 9be0f4a6f155 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Aug 01 09:31:10 2011 -0700
+++ b/src/HOL/SetInterval.thy	Mon Aug 01 19:53:30 2011 +0200
@@ -14,6 +14,7 @@
 
 context ord
 begin
+
 definition
   lessThan    :: "'a => 'a set" ("(1{..<_})") where
   "{..<u} == {x. x < u}"
@@ -1162,12 +1163,18 @@
           (if m <= n then f m - f(n + 1) else 0)"
 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
 
-lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def]
+lemma setsum_restrict_set':
+  "finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)"
+  by (simp add: setsum_restrict_set [symmetric] Int_def)
+
+lemma setsum_restrict_set'':
+  "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
+  by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])
 
 lemma setsum_setsum_restrict:
-  "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"
-  by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def)
-     (rule setsum_commute)
+  "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"
+  by (simp add: setsum_restrict_set'') (rule setsum_commute)
 
 lemma setsum_image_gen: assumes fS: "finite S"
   shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"