author hoelzl Fri Dec 03 00:36:01 2010 +0100 (2010-12-03) changeset 40897 1eb1b2f9d062 parent 40892 6f7292b94652 child 40898 882e860a1e83
adapt proofs to changed set_plus_image (cf. ee8d0548c148);
```     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Dec 02 21:23:56 2010 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Dec 03 00:36:01 2010 +0100
1.3 @@ -313,7 +313,7 @@
1.4
1.5  lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
1.6
1.7 -lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps)
1.8 +lemma fst_snd_linear: "linear (%(x,y). x + y)" unfolding linear_def by (simp add: algebra_simps)
1.9
1.10  lemma scaleR_2:
1.11    fixes x :: "'a::real_vector"
1.12 @@ -5451,11 +5451,11 @@
1.13  shows "convex hull (S \<oplus> T) = (convex hull S) \<oplus> (convex hull T)"
1.14  proof-
1.15  have "(convex hull S) \<oplus> (convex hull T) =
1.16 -      (%z. fst z + snd z) ` ((convex hull S) <*> (convex hull T))"
1.17 +      (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
1.19 -also have "... = (%z. fst z + snd z) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
1.20 +also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
1.21  also have "...= convex hull (S \<oplus> T)" using fst_snd_linear linear_conv_bounded_linear
1.22 -   convex_hull_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
1.23 +   convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
1.24  finally show ?thesis by auto
1.25  qed
1.26
1.27 @@ -5464,11 +5464,11 @@
1.28  assumes "convex S" "convex T"
1.29  shows "rel_interior (S \<oplus> T) = (rel_interior S) \<oplus> (rel_interior T)"
1.30  proof-
1.31 -have "(rel_interior S) \<oplus> (rel_interior T) = (%z. fst z + snd z) ` (rel_interior S <*> rel_interior T)"
1.32 +have "(rel_interior S) \<oplus> (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"