# HG changeset patch
# User hoelzl
# Date 1291332961 -3600
# Node ID 1eb1b2f9d0625c1beb3aaa4539bc357d31b6f186
# Parent  6f7292b946520a732ae74d7826de59e1bc8105e9
adapt proofs to changed set_plus_image (cf. ee8d0548c148);

diff -r 6f7292b94652 -r 1eb1b2f9d062 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Dec 02 21:23:56 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Dec 03 00:36:01 2010 +0100
@@ -313,7 +313,7 @@
 
 lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
 
-lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps)
+lemma fst_snd_linear: "linear (%(x,y). x + y)" unfolding linear_def by (simp add: algebra_simps)
 
 lemma scaleR_2:
   fixes x :: "'a::real_vector"
@@ -5451,11 +5451,11 @@
 shows "convex hull (S \<oplus> T) = (convex hull S) \<oplus> (convex hull T)"
 proof-
 have "(convex hull S) \<oplus> (convex hull T) =
-      (%z. fst z + snd z) ` ((convex hull S) <*> (convex hull T))"
+      (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
    by (simp add: set_plus_image)
-also have "... = (%z. fst z + snd z) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
+also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
 also have "...= convex hull (S \<oplus> T)" using fst_snd_linear linear_conv_bounded_linear
-   convex_hull_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
+   convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
 finally show ?thesis by auto
 qed
 
@@ -5464,11 +5464,11 @@
 assumes "convex S" "convex T"
 shows "rel_interior (S \<oplus> T) = (rel_interior S) \<oplus> (rel_interior T)"
 proof-
-have "(rel_interior S) \<oplus> (rel_interior T) = (%z. fst z + snd z) ` (rel_interior S <*> rel_interior T)"
+have "(rel_interior S) \<oplus> (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
    by (simp add: set_plus_image)
-also have "... = (%z. fst z + snd z) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
+also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
 also have "...= rel_interior (S \<oplus> T)" using fst_snd_linear convex_direct_sum assms
-   rel_interior_convex_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
+   rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
 finally show ?thesis by auto
 qed