# HG changeset patch
# User wenzelm
# Date 1393518286 -3600
# Node ID 41a73a41f6c82b3674527542d3424bc8a2aaae17
# Parent  96861130f922ebdcc23f76c226f6adcb8953bdf0
more symbols;

diff -r 96861130f922 -r 41a73a41f6c8 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Feb 27 17:24:16 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Feb 27 17:24:46 2014 +0100
@@ -8137,7 +8137,7 @@
     then have "rel_interior (S \<times> T) = rel_interior ((S \<times> (UNIV :: 'm set)) \<inter> ((UNIV :: 'n set) \<times> T))"
       by auto
     also have "\<dots> = rel_interior (S \<times> (UNIV :: 'm set)) \<inter> rel_interior ((UNIV :: 'n set) \<times> T)"
-       apply (subst convex_rel_interior_inter_two[of "S \<times> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"])
+       apply (subst convex_rel_interior_inter_two[of "S \<times> (UNIV :: 'm set)" "(UNIV :: 'n set) \<times> T"])
        using * ri assms convex_Times
        apply auto
        done
@@ -8338,7 +8338,7 @@
 lemma rel_interior_convex_cone_aux:
   fixes S :: "'m::euclidean_space set"
   assumes "convex S"
-  shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} <*> S)) \<longleftrightarrow>
+  shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow>
     c > 0 \<and> x \<in> ((op *\<^sub>R c) ` (rel_interior S))"
 proof (cases "S = {}")
   case True
@@ -8347,33 +8347,33 @@
 next
   case False
   then obtain s where "s \<in> S" by auto
-  have conv: "convex ({(1 :: real)} <*> S)"
+  have conv: "convex ({(1 :: real)} \<times> S)"
     using convex_Times[of "{(1 :: real)}" S] assms convex_singleton[of "1 :: real"]
     by auto
-  def f \<equiv> "\<lambda>y. {z. (y, z) \<in> cone hull ({1 :: real} <*> S)}"
-  then have *: "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} <*> S)) =
+  def f \<equiv> "\<lambda>y. {z. (y, z) \<in> cone hull ({1 :: real} \<times> S)}"
+  then have *: "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) =
     (c \<in> rel_interior {y. f y \<noteq> {}} \<and> x \<in> rel_interior (f c))"
-    apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} <*> S)" f c x])
-    using convex_cone_hull[of "{(1 :: real)} <*> S"] conv
+    apply (subst rel_interior_projection[of "cone hull ({(1 :: real)} \<times> S)" f c x])
+    using convex_cone_hull[of "{(1 :: real)} \<times> S"] conv
     apply auto
     done
   {
     fix y :: real
     assume "y \<ge> 0"
-    then have "y *\<^sub>R (1,s) \<in> cone hull ({1 :: real} <*> S)"
-      using cone_hull_expl[of "{(1 :: real)} <*> S"] `s \<in> S` by auto
+    then have "y *\<^sub>R (1,s) \<in> cone hull ({1 :: real} \<times> S)"
+      using cone_hull_expl[of "{(1 :: real)} \<times> S"] `s \<in> S` by auto
     then have "f y \<noteq> {}"
       using f_def by auto
   }
   then have "{y. f y \<noteq> {}} = {0..}"
-    using f_def cone_hull_expl[of "{1 :: real} <*> S"] by auto
+    using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
   then have **: "rel_interior {y. f y \<noteq> {}} = {0<..}"
     using rel_interior_real_semiline by auto
   {
     fix c :: real
     assume "c > 0"
     then have "f c = (op *\<^sub>R c ` S)"
-      using f_def cone_hull_expl[of "{1 :: real} <*> S"] by auto
+      using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
     then have "rel_interior (f c) = op *\<^sub>R c ` rel_interior S"
       using rel_interior_convex_scaleR[of S c] assms by auto
   }
@@ -8383,7 +8383,7 @@
 lemma rel_interior_convex_cone:
   fixes S :: "'m::euclidean_space set"
   assumes "convex S"
-  shows "rel_interior (cone hull ({1 :: real} <*> S)) =
+  shows "rel_interior (cone hull ({1 :: real} \<times> S)) =
     {(c, c *\<^sub>R x) | c x. c > 0 \<and> x \<in> rel_interior S}"
   (is "?lhs = ?rhs")
 proof -
@@ -8621,13 +8621,13 @@
   fixes S T :: "'n::euclidean_space set"
   shows "convex hull (S + T) = convex hull S + convex hull T"
 proof -
-  have "convex hull S + convex hull T = (\<lambda>(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
+  have "convex hull S + convex hull T = (\<lambda>(x,y). x + y) ` ((convex hull S) \<times> (convex hull T))"
     by (simp add: set_plus_image)
-  also have "\<dots> = (\<lambda>(x,y). x + y) ` (convex hull (S <*> T))"
+  also have "\<dots> = (\<lambda>(x,y). x + y) ` (convex hull (S \<times> T))"
     using convex_hull_Times by auto
   also have "\<dots> = convex hull (S + T)"
     using fst_snd_linear linear_conv_bounded_linear
-      convex_hull_linear_image[of "(\<lambda>(x,y). x + y)" "S <*> T"]
+      convex_hull_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"]
     by (auto simp add: set_plus_image)
   finally show ?thesis ..
 qed
@@ -8638,13 +8638,13 @@
     and "convex T"
   shows "rel_interior (S + T) = rel_interior S + rel_interior T"
 proof -
-  have "rel_interior S + rel_interior T = (\<lambda>(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
+  have "rel_interior S + rel_interior T = (\<lambda>(x,y). x + y) ` (rel_interior S \<times> rel_interior T)"
     by (simp add: set_plus_image)
-  also have "\<dots> = (\<lambda>(x,y). x + y) ` rel_interior (S <*> T)"
+  also have "\<dots> = (\<lambda>(x,y). x + y) ` rel_interior (S \<times> T)"
     using rel_interior_direct_sum assms by auto
   also have "\<dots> = rel_interior (S + T)"
     using fst_snd_linear convex_Times assms
-      rel_interior_convex_linear_image[of "(\<lambda>(x,y). x + y)" "S <*> T"]
+      rel_interior_convex_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"]
     by (auto simp add: set_plus_image)
   finally show ?thesis ..
 qed
@@ -8685,7 +8685,7 @@
     and "rel_open S"
     and "convex T"
     and "rel_open T"
-  shows "convex (S <*> T) \<and> rel_open (S <*> T)"
+  shows "convex (S \<times> T) \<and> rel_open (S \<times> T)"
   by (metis assms convex_Times rel_interior_direct_sum rel_open_def)
 
 lemma convex_rel_open_sum:
@@ -8799,8 +8799,8 @@
   def C0 \<equiv> "convex hull (\<Union>(S ` I))"
   have "\<forall>i\<in>I. C0 \<ge> S i"
     unfolding C0_def using hull_subset[of "\<Union>(S ` I)"] by auto
-  def K0 \<equiv> "cone hull ({1 :: real} <*> C0)"
-  def K \<equiv> "\<lambda>i. cone hull ({1 :: real} <*> S i)"
+  def K0 \<equiv> "cone hull ({1 :: real} \<times> C0)"
+  def K \<equiv> "\<lambda>i. cone hull ({1 :: real} \<times> S i)"
   have "\<forall>i\<in>I. K i \<noteq> {}"
     unfolding K_def using assms
     by (simp add: cone_hull_empty_iff[symmetric])
@@ -8838,13 +8838,13 @@
     done
   ultimately have geq: "K0 \<supseteq> convex hull (\<Union>(K ` I))"
     using hull_minimal[of _ "K0" "convex"] by blast
-  have "\<forall>i\<in>I. K i \<supseteq> {1 :: real} <*> S i"
+  have "\<forall>i\<in>I. K i \<supseteq> {1 :: real} \<times> S i"
     using K_def by (simp add: hull_subset)
-  then have "\<Union>(K ` I) \<supseteq> {1 :: real} <*> \<Union>(S ` I)"
+  then have "\<Union>(K ` I) \<supseteq> {1 :: real} \<times> \<Union>(S ` I)"
     by auto
-  then have "convex hull \<Union>(K ` I) \<supseteq> convex hull ({1 :: real} <*> \<Union>(S ` I))"
+  then have "convex hull \<Union>(K ` I) \<supseteq> convex hull ({1 :: real} \<times> \<Union>(S ` I))"
     by (simp add: hull_mono)
-  then have "convex hull \<Union>(K ` I) \<supseteq> {1 :: real} <*> C0"
+  then have "convex hull \<Union>(K ` I) \<supseteq> {1 :: real} \<times> C0"
     unfolding C0_def
     using convex_hull_Times[of "{(1 :: real)}" "\<Union>(S ` I)"] convex_hull_singleton
     by auto
@@ -8889,7 +8889,7 @@
     {
       fix i
       assume "i \<in> I"
-      then have "convex (S i) \<and> k i \<in> rel_interior (cone hull {1} <*> S i)"
+      then have "convex (S i) \<and> k i \<in> rel_interior (cone hull {1} \<times> S i)"
         using k K_def assms by auto
       then have "\<exists>ci si. k i = (ci, ci *\<^sub>R si) \<and> 0 < ci \<and> si \<in> rel_interior (S i)"
         using rel_interior_convex_cone[of "S i"] by auto