src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 44170 510ac30f44c0
parent 44142 8e27e0177518
child 44282 f0de18b62d63
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Aug 12 07:18:28 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Aug 12 09:17:24 2011 -0700
     1.3 @@ -101,9 +101,9 @@
     1.4  
     1.5  lemma span_eq[simp]: "(span s = s) <-> subspace s"
     1.6  proof-
     1.7 -  { fix f assume "f <= subspace"
     1.8 -    hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto  }
     1.9 -  thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto
    1.10 +  { fix f assume "Ball f subspace"
    1.11 +    hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto  }
    1.12 +  thus ?thesis using hull_eq[of subspace s] span_def by auto
    1.13  qed
    1.14  
    1.15  lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
    1.16 @@ -391,11 +391,11 @@
    1.17    unfolding affine_def by auto
    1.18  
    1.19  lemma affine_affine_hull: "affine(affine hull s)"
    1.20 -  unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"]
    1.21 -  unfolding mem_def by auto
    1.22 +  unfolding hull_def using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"]
    1.23 +  by auto
    1.24  
    1.25  lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
    1.26 -by (metis affine_affine_hull hull_same mem_def)
    1.27 +by (metis affine_affine_hull hull_same)
    1.28  
    1.29  subsection {* Some explicit formulations (from Lars Schewe). *}
    1.30  
    1.31 @@ -459,7 +459,7 @@
    1.32  
    1.33  lemma affine_hull_explicit:
    1.34    "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}"
    1.35 -  apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine]
    1.36 +  apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq
    1.37    apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-
    1.38    fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
    1.39      apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
    1.40 @@ -500,7 +500,7 @@
    1.41  subsection {* Stepping theorems and hence small special cases. *}
    1.42  
    1.43  lemma affine_hull_empty[simp]: "affine hull {} = {}"
    1.44 -  apply(rule hull_unique) unfolding mem_def by auto
    1.45 +  apply(rule hull_unique) by auto
    1.46  
    1.47  lemma affine_hull_finite_step:
    1.48    fixes y :: "'a::real_vector"
    1.49 @@ -812,12 +812,11 @@
    1.50  subsection {* Conic hull. *}
    1.51  
    1.52  lemma cone_cone_hull: "cone (cone hull s)"
    1.53 -  unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"] 
    1.54 -  by (auto simp add: mem_def)
    1.55 +  unfolding hull_def by auto
    1.56  
    1.57  lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"
    1.58 -  apply(rule hull_eq[unfolded mem_def])
    1.59 -  using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
    1.60 +  apply(rule hull_eq)
    1.61 +  using cone_Inter unfolding subset_eq by auto
    1.62  
    1.63  lemma mem_cone:
    1.64    assumes "cone S" "x : S" "c>=0"
    1.65 @@ -888,7 +887,7 @@
    1.66  lemma mem_cone_hull:
    1.67    assumes "x : S" "c>=0"
    1.68    shows "c *\<^sub>R x : cone hull S"
    1.69 -by (metis assms cone_cone_hull hull_inc mem_cone mem_def)
    1.70 +by (metis assms cone_cone_hull hull_inc mem_cone)
    1.71  
    1.72  lemma cone_hull_expl:
    1.73  fixes S :: "('m::euclidean_space) set"
    1.74 @@ -901,11 +900,11 @@
    1.75    moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto
    1.76    ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto
    1.77  } hence "cone ?rhs" unfolding cone_def by auto
    1.78 -  hence "?rhs : cone" unfolding mem_def by auto
    1.79 +  hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto
    1.80  { fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto
    1.81    hence "x : ?rhs" by auto
    1.82  } hence "S <= ?rhs" by auto
    1.83 -hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto
    1.84 +hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto
    1.85  moreover
    1.86  { fix x assume "x : ?rhs"
    1.87    from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
    1.88 @@ -1081,18 +1080,18 @@
    1.89  subsection {* Convex hull. *}
    1.90  
    1.91  lemma convex_convex_hull: "convex(convex hull s)"
    1.92 -  unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
    1.93 -  unfolding mem_def by auto
    1.94 +  unfolding hull_def using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
    1.95 +  by auto
    1.96  
    1.97  lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
    1.98 -by (metis convex_convex_hull hull_same mem_def)
    1.99 +by (metis convex_convex_hull hull_same)
   1.100  
   1.101  lemma bounded_convex_hull:
   1.102    fixes s :: "'a::real_normed_vector set"
   1.103    assumes "bounded s" shows "bounded(convex hull s)"
   1.104  proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
   1.105    show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
   1.106 -    unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
   1.107 +    unfolding subset_hull[of convex, OF convex_cball]
   1.108      unfolding subset_eq mem_cball dist_norm using B by auto qed
   1.109  
   1.110  lemma finite_imp_bounded_convex_hull:
   1.111 @@ -1125,17 +1124,17 @@
   1.112  subsection {* Stepping theorems for convex hulls of finite sets. *}
   1.113  
   1.114  lemma convex_hull_empty[simp]: "convex hull {} = {}"
   1.115 -  apply(rule hull_unique) unfolding mem_def by auto
   1.116 +  apply(rule hull_unique) by auto
   1.117  
   1.118  lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
   1.119 -  apply(rule hull_unique) unfolding mem_def by auto
   1.120 +  apply(rule hull_unique) by auto
   1.121  
   1.122  lemma convex_hull_insert:
   1.123    fixes s :: "'a::real_vector set"
   1.124    assumes "s \<noteq> {}"
   1.125    shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
   1.126                                      b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
   1.127 - apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof-
   1.128 + apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof-
   1.129   fix x assume x:"x = a \<or> x \<in> s"
   1.130   thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer 
   1.131     apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
   1.132 @@ -1192,7 +1191,7 @@
   1.133    shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
   1.134                              (setsum u {1..k} = 1) \<and>
   1.135                              (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
   1.136 -  apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
   1.137 +  apply(rule hull_unique) apply(rule) defer
   1.138    apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
   1.139  proof-
   1.140    fix x assume "x\<in>s"
   1.141 @@ -1232,7 +1231,7 @@
   1.142    assumes "finite s"
   1.143    shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
   1.144           setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
   1.145 -proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
   1.146 +proof(rule hull_unique, auto simp add: convex_def[of ?set])
   1.147    fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x" 
   1.148      apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
   1.149      unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto 
   1.150 @@ -1356,8 +1355,8 @@
   1.151    apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed
   1.152  
   1.153  lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u.  0 \<le> u \<and> u \<le> 1}"
   1.154 -  unfolding convex_hull_2 unfolding Collect_def 
   1.155 -proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
   1.156 +  unfolding convex_hull_2
   1.157 +proof(rule Collect_cong) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
   1.158    fix x show "(\<exists>v u. x = v *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> v \<and> 0 \<le> u \<and> v + u = 1) = (\<exists>u. x = a + u *\<^sub>R (b - a) \<and> 0 \<le> u \<and> u \<le> 1)"
   1.159      unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed
   1.160  
   1.161 @@ -1367,8 +1366,8 @@
   1.162    have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
   1.163    have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
   1.164           "\<And>x y z ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps)
   1.165 -  show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
   1.166 -    unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
   1.167 +  show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and *
   1.168 +    unfolding convex_hull_finite_step[OF fin(3)] apply(rule Collect_cong) apply simp apply auto
   1.169      apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
   1.170      apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed
   1.171  
   1.172 @@ -1392,14 +1391,14 @@
   1.173  
   1.174  lemma affine_hull_subset_span:
   1.175    fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)"
   1.176 -by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span)
   1.177 +by (metis hull_minimal span_inc subspace_imp_affine subspace_span)
   1.178  
   1.179  lemma convex_hull_subset_span:
   1.180    fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)"
   1.181 -by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span)
   1.182 +by (metis hull_minimal span_inc subspace_imp_convex subspace_span)
   1.183  
   1.184  lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
   1.185 -by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def)
   1.186 +by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
   1.187  
   1.188  
   1.189  lemma affine_dependent_imp_dependent:
   1.190 @@ -1572,11 +1571,11 @@
   1.191  proof-
   1.192  have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto
   1.193  moreover have "(%x. a + x) `  S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto
   1.194 -ultimately have h1: "affine hull ((%x. a + x) `  S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def)
   1.195 +ultimately have h1: "affine hull ((%x. a + x) `  S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal)
   1.196  have "affine((%x. -a + x) ` (affine hull ((%x. a + x) `  S)))"  using affine_translation affine_affine_hull by auto
   1.197  moreover have "(%x. -a + x) ` (%x. a + x) `  S <= (%x. -a + x) ` (affine hull ((%x. a + x) `  S))" using hull_subset[of "(%x. a + x) `  S"] by auto 
   1.198  moreover have "S=(%x. -a + x) ` (%x. a + x) `  S" using  translation_assoc[of "-a" a] by auto
   1.199 -ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) `  S)) >= (affine hull S)" by (metis hull_minimal mem_def)
   1.200 +ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) `  S)) >= (affine hull S)" by (metis hull_minimal)
   1.201  hence "affine hull ((%x. a + x) `  S) >= (%x. a + x) ` (affine hull S)" by auto
   1.202  from this show ?thesis using h1 by auto
   1.203  qed
   1.204 @@ -3016,7 +3015,7 @@
   1.205      then obtain a b where ab:"a \<noteq> 0" "0 < b"  "\<forall>x\<in>convex hull c. b < inner a x"
   1.206        using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
   1.207        using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
   1.208 -      using subset_hull[unfolded mem_def, of convex, OF assms(1), THEN sym, of c] by auto
   1.209 +      using subset_hull[of convex, OF assms(1), THEN sym, of c] by auto
   1.210      hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
   1.211         using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
   1.212         apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
   1.213 @@ -3077,7 +3076,7 @@
   1.214  
   1.215  lemma convex_hull_translation_lemma:
   1.216    "convex hull ((\<lambda>x. a + x) ` s) \<subseteq> (\<lambda>x. a + x) ` (convex hull s)"
   1.217 -by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono mem_def)
   1.218 +by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono)
   1.219  
   1.220  lemma convex_hull_bilemma: fixes neg
   1.221    assumes "(\<forall>s a. (convex hull (up a s)) \<subseteq> up a (convex hull s))"
   1.222 @@ -3091,7 +3090,7 @@
   1.223  
   1.224  lemma convex_hull_scaling_lemma:
   1.225   "(convex hull ((\<lambda>x. c *\<^sub>R x) ` s)) \<subseteq> (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
   1.226 -by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff)
   1.227 +by (metis convex_convex_hull convex_scaling hull_subset subset_hull subset_image_iff)
   1.228  
   1.229  lemma convex_hull_scaling:
   1.230    "convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
   1.231 @@ -3269,7 +3268,7 @@
   1.232        unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
   1.233      have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
   1.234      have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
   1.235 -      apply(rule_tac [!] hull_minimal) using Suc gh(3-4)  unfolding mem_def unfolding subset_eq
   1.236 +      apply(rule_tac [!] hull_minimal) using Suc gh(3-4)  unfolding subset_eq
   1.237        apply(rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) apply rule prefer 3 apply rule proof-
   1.238        fix x assume "x\<in>X ` g" then guess y unfolding image_iff ..
   1.239        thus "x\<in>\<Inter>h" using X[THEN bspec[where x=y]] using * f by auto next
   1.240 @@ -3710,7 +3709,7 @@
   1.241      apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **) 
   1.242      apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
   1.243      unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
   1.244 -    by(auto simp add: mem_def[of _ convex]) qed
   1.245 +    by auto qed
   1.246  
   1.247  subsection {* And this is a finite set of vertices. *}
   1.248  
   1.249 @@ -3883,7 +3882,7 @@
   1.250    closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   1.251    "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
   1.252  
   1.253 -definition "between = (\<lambda> (a,b). closed_segment a b)"
   1.254 +definition "between = (\<lambda> (a,b) x. x \<in> closed_segment a b)"
   1.255  
   1.256  lemmas segment = open_segment_def closed_segment_def
   1.257  
   1.258 @@ -3968,15 +3967,15 @@
   1.259  lemma segment_refl:"closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps)
   1.260  
   1.261  lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   1.262 -  unfolding between_def mem_def by auto
   1.263 +  unfolding between_def by auto
   1.264  
   1.265  lemma between:"between (a,b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
   1.266  proof(cases "a = b")
   1.267 -  case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
   1.268 +  case True thus ?thesis unfolding between_def split_conv
   1.269      by(auto simp add:segment_refl dist_commute) next
   1.270    case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto 
   1.271    have *:"\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps)
   1.272 -  show ?thesis unfolding between_def split_conv mem_def[of x, symmetric] closed_segment_def mem_Collect_eq
   1.273 +  show ?thesis unfolding between_def split_conv closed_segment_def mem_Collect_eq
   1.274      apply rule apply(erule exE, (erule conjE)+) apply(subst dist_triangle_eq) proof-
   1.275        fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" 
   1.276        hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
   1.277 @@ -4743,8 +4742,8 @@
   1.278    { fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto }
   1.279    hence "y : Inter {closure S |S. S : I}" by auto
   1.280  } hence "Inter I <= Inter {closure S |S. S : I}" by auto
   1.281 -moreover have "Inter {closure S |S. S : I} : closed" 
   1.282 -  unfolding mem_def closed_Inter closed_closure by auto
   1.283 +moreover have "closed (Inter {closure S |S. S : I})"
   1.284 +  unfolding closed_Inter closed_closure by auto
   1.285  ultimately show ?thesis using closure_hull[of "Inter I"]
   1.286    hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto
   1.287  qed
   1.288 @@ -5074,8 +5073,8 @@
   1.289       using I_def u_def by auto
   1.290  }
   1.291  hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto
   1.292 -moreover have "(convex hull S) <*> (convex hull T) : convex" 
   1.293 -   unfolding mem_def by (simp add: convex_direct_sum convex_convex_hull)
   1.294 +moreover have "convex ((convex hull S) <*> (convex hull T))" 
   1.295 +   by (simp add: convex_direct_sum convex_convex_hull)
   1.296  ultimately show ?thesis 
   1.297     using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"] 
   1.298           hull_subset[of S convex] hull_subset[of T convex] by auto
   1.299 @@ -5384,7 +5383,6 @@
   1.300    finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto
   1.301    hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto
   1.302  } hence "convex ?rhs" unfolding convex_def by auto
   1.303 -hence "?rhs : convex" unfolding mem_def by auto
   1.304  from this show ?thesis using `?lhs >= ?rhs` * 
   1.305     hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast
   1.306  qed
   1.307 @@ -5578,7 +5576,7 @@
   1.308      hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto
   1.309    }
   1.310    hence "K0 >= Union (K ` I)" by auto
   1.311 -  moreover have "K0 : convex" unfolding mem_def K0_def
   1.312 +  moreover have "convex K0" unfolding K0_def
   1.313       apply (subst convex_cone_hull) apply (subst convex_direct_sum)
   1.314       unfolding C0_def using convex_convex_hull by auto
   1.315    ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
   1.316 @@ -5587,7 +5585,7 @@
   1.317    hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
   1.318    hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
   1.319       using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
   1.320 -  moreover have "convex hull(Union (K ` I)) : cone" unfolding mem_def apply (subst cone_convex_hull)
   1.321 +  moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull)
   1.322       using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
   1.323    ultimately have "convex hull (Union (K ` I)) >= K0"
   1.324       unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast