# HG changeset patch
# User wenzelm
# Date 1357825219 -3600
# Node ID 4156a45aeb638c3a2235c7ba5b4fd1183601f305
# Parent  8a1ea6b00aced0a84e78a07bf5b01041dc6639f8
tuned proofs;

diff -r 8a1ea6b00ace -r 4156a45aeb63 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Jan 10 13:15:05 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Jan 10 14:40:19 2013 +0100
@@ -125,8 +125,8 @@
   { fix x :: "'n::euclidean_space"
     def y == "(e/norm x) *\<^sub>R x"
     then have "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto
-    moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
-    moreover hence "x = (norm x/e) *\<^sub>R y" by auto
+    moreover have *: "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
+    moreover from * have "x = (norm x/e) *\<^sub>R y" by auto
     ultimately have "x : span (cball 0 e)"
       using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
   } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto
@@ -297,7 +297,7 @@
     and "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
     and "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"
     and "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
-  apply(rule_tac [!] setsum_cong2)
+  apply (rule_tac [!] setsum_cong2)
   using assms apply auto
   done
 
@@ -659,12 +659,12 @@
 qed
 
 lemma mem_affine:
-  assumes "affine S" "x : S" "y : S" "u+v=1"
+  assumes "affine S" "x : S" "y : S" "u + v = 1"
   shows "(u *\<^sub>R x + v *\<^sub>R y) : S"
   using assms affine_def[of S] by auto
 
 lemma mem_affine_3:
-  assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1"
+  assumes "affine S" "x : S" "y : S" "z : S" "u + v + w = 1"
   shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S"
 proof -
   have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}"
@@ -689,7 +689,9 @@
   "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
   unfolding subset_eq Ball_def
   unfolding affine_hull_explicit span_explicit mem_Collect_eq
-  apply (rule, rule) apply (erule exE)+ apply (erule conjE)+
+  apply (rule, rule)
+  apply (erule exE)+
+  apply (erule conjE)+
 proof -
   fix x t u
   assume as: "finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
@@ -1163,90 +1165,109 @@
   shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
 proof -
   let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
-  have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)
+  have Se: " \<exists>x. x \<in> ?S"
+    apply (rule exI[where x=a])
+    apply (auto simp add: fa)
+    done
   have Sub: "\<exists>y. isUb UNIV ?S y"
     apply (rule exI[where x= b])
-    using ab fb e12 by (auto simp add: isUb_def setle_def)
+    using ab fb e12 apply (auto simp add: isUb_def setle_def)
+    done
   from reals_complete[OF Se Sub] obtain l where
     l: "isLub UNIV ?S l"by blast
   have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12
     apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-    by (metis linorder_linear)
+    apply (metis linorder_linear)
+    done
   have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l
     apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-    by (metis linorder_linear not_le)
-    have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
-    have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
-    have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
-    then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
-    {assume le2: "f l \<in> e2"
-      from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
-      hence lap: "l - a > 0" using alb by arith
-      from e2[rule_format, OF le2] obtain e where
-        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
-      from dst[OF alb e(1)] obtain d where
-        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      let ?d' = "min (d/2) ((l - a)/2)"
-      have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
-        by (simp add: min_max.less_infI2)
-      then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
-      then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
-      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
-      from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
-      moreover
-      have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
-      ultimately have False using e12 alb d' by auto}
+    apply (metis linorder_linear not_le)
+    done
+  have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
+  have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
+  have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
+  then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
+  { assume le2: "f l \<in> e2"
+    from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
+    then have lap: "l - a > 0" using alb by arith
+    from e2[rule_format, OF le2] obtain e where
+      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
+    from dst[OF alb e(1)] obtain d where
+      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+    let ?d' = "min (d/2) ((l - a)/2)"
+    have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
+      by (simp add: min_max.less_infI2)
+    then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
+    then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
+    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
+    from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
     moreover
-    {assume le1: "f l \<in> e1"
+    have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
+    ultimately have False using e12 alb d' by auto }
+  moreover
+  { assume le1: "f l \<in> e1"
     from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
-      hence blp: "b - l > 0" using alb by arith
-      from e1[rule_format, OF le1] obtain e where
-        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
-      from dst[OF alb e(1)] obtain d where
-        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
-      then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
-      then obtain d' where d': "d' > 0" "d' < d" by metis
-      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
-      hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
-      with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
-      with l d' have False
-        by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
-    ultimately show ?thesis using alb by metis
+    then have blp: "b - l > 0" using alb by arith
+    from e1[rule_format, OF le1] obtain e where
+      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
+    from dst[OF alb e(1)] obtain d where
+      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+    have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
+    then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
+    then obtain d' where d': "d' > 0" "d' < d" by metis
+    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
+    then have "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
+    with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
+    with l d' have False
+      by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
+  ultimately show ?thesis using alb by metis
 qed
 
 lemma convex_connected:
   fixes s :: "'a::real_normed_vector set"
   assumes "convex s" shows "connected s"
-proof-
-  { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
+proof -
+  { fix e1 e2
+    assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
     assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
     then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto
-    hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
+    then have n: "norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
 
     { fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e"
-      { fix y have *:"(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2"
+      { fix y
+        have *: "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2"
           by (simp add: algebra_simps)
         assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
         hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
           unfolding * and scaleR_right_diff_distrib[symmetric]
-          unfolding less_divide_eq using n by auto  }
-      hence "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
-        apply(rule_tac x="e / norm (x1 - x2)" in exI) using as
-        apply auto unfolding zero_less_divide_iff using n by simp  }  note * = this
+          unfolding less_divide_eq using n by auto
+      }
+      then have "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
+        apply (rule_tac x="e / norm (x1 - x2)" in exI)
+        using as
+        apply auto
+        unfolding zero_less_divide_iff
+        using n apply simp
+        done
+    } note * = this
 
     have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
-      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
-      using * apply(simp add: dist_norm)
+      apply (rule connected_real_lemma)
+      apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
+      using * apply (simp add: dist_norm)
       using as(1,2)[unfolded open_dist] apply simp
       using as(1,2)[unfolded open_dist] apply simp
       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
-      using as(3) by auto
-    then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1"  "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" by auto
-    hence False using as(4)
+      using as(3) apply auto
+      done
+    then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1"  "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
+      by auto
+    then have False
+      using as(4)
       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]
-      using x1(2) x2(2) by auto  }
-  thus ?thesis unfolding connected_def by auto
+      using x1(2) x2(2) by auto
+    }
+  then show ?thesis unfolding connected_def by auto
 qed
 
 text {* One rather trivial consequence. *}
@@ -1276,37 +1297,53 @@
   hence xy:"0 < dist x y" by (auto simp add: dist_nz[symmetric])
 
   then obtain u where "0 < u" "u \<le> 1" and u:"u < e / dist x y"
-    using real_lbound_gt_zero[of 1 "e / dist x y"] using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto
+    using real_lbound_gt_zero[of 1 "e / dist x y"]
+    using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto
   hence "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y" using `x\<in>s` `y\<in>s`
-    using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto
+    using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]]
+    by auto
   moreover
-  have *:"x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" by (simp add: algebra_simps)
-  have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`] unfolding dist_norm[symmetric]
+  have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
+    by (simp add: algebra_simps)
+  have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e"
+    unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`]
+    unfolding dist_norm[symmetric]
     using u unfolding pos_less_divide_eq[OF xy] by auto
-  hence "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto
-  ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
+  then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto
+  ultimately show False
+    using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
 qed
 
 lemma convex_ball:
   fixes x :: "'a::real_normed_vector"
   shows "convex (ball x e)"
-proof(auto simp add: convex_def)
-  fix y z assume yz:"dist x y < e" "dist x z < e"
-  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
-  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
-    using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
-  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto
+proof (auto simp add: convex_def)
+  fix y z
+  assume yz: "dist x y < e" "dist x z < e"
+  fix u v :: real
+  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
+    using uv yz
+    using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]]
+    by auto
+  then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
+    using convex_bound_lt[OF yz uv] by auto
 qed
 
 lemma convex_cball:
   fixes x :: "'a::real_normed_vector"
   shows "convex(cball x e)"
-proof(auto simp add: convex_def Ball_def)
-  fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"
-  fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
-  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
-    using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
-  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto
+proof (auto simp add: convex_def Ball_def)
+  fix y z
+  assume yz: "dist x y \<le> e" "dist x z \<le> e"
+  fix u v :: real
+  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
+    using uv yz
+    using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]]
+    by auto
+  then show "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
+    using convex_bound_le[OF yz uv] by auto
 qed
 
 lemma connected_ball:
@@ -1319,6 +1356,7 @@
   shows "connected(cball x e)"
   using convex_connected convex_cball by auto
 
+
 subsection {* Convex hull *}
 
 lemma convex_convex_hull: "convex(convex hull s)"
@@ -1326,102 +1364,182 @@
   by auto
 
 lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
-by (metis convex_convex_hull hull_same)
+  by (metis convex_convex_hull hull_same)
 
 lemma bounded_convex_hull:
   fixes s :: "'a::real_normed_vector set"
   assumes "bounded s" shows "bounded(convex hull s)"
-proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
-  show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
+proof -
+  from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
+    unfolding bounded_iff by auto
+  show ?thesis
+    apply (rule bounded_subset[OF bounded_cball, of _ 0 B])
     unfolding subset_hull[of convex, OF convex_cball]
-    unfolding subset_eq mem_cball dist_norm using B by auto qed
+    unfolding subset_eq mem_cball dist_norm using B apply auto
+    done
+qed
 
 lemma finite_imp_bounded_convex_hull:
   fixes s :: "'a::real_normed_vector set"
   shows "finite s \<Longrightarrow> bounded(convex hull s)"
   using bounded_convex_hull finite_imp_bounded by auto
 
+
 subsubsection {* Convex hull is "preserved" by a linear function *}
 
 lemma convex_hull_linear_image:
   assumes "bounded_linear f"
   shows "f ` (convex hull s) = convex hull (f ` s)"
-  apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
-  apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
-  apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
-proof-
+  apply rule
+  unfolding subset_eq ball_simps
+  apply (rule_tac[!] hull_induct, rule hull_inc)
+  prefer 3
+  apply (erule imageE)
+  apply (rule_tac x=xa in image_eqI)
+  apply assumption
+  apply (rule hull_subset[unfolded subset_eq, rule_format])
+  apply assumption
+proof -
   interpret f: bounded_linear f by fact
   show "convex {x. f x \<in> convex hull f ` s}"
-  unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
+    unfolding convex_def
+    by (auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format])
+next
   interpret f: bounded_linear f by fact
-  show "convex {x. x \<in> f ` (convex hull s)}" using  convex_convex_hull[unfolded convex_def, of s]
+  show "convex {x. x \<in> f ` (convex hull s)}"
+    using  convex_convex_hull[unfolded convex_def, of s]
     unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
 qed auto
 
 lemma in_convex_hull_linear_image:
   assumes "bounded_linear f" "x \<in> convex hull s"
   shows "(f x) \<in> convex hull (f ` s)"
-using convex_hull_linear_image[OF assms(1)] assms(2) by auto
+  using convex_hull_linear_image[OF assms(1)] assms(2) by auto
+
 
 subsubsection {* Stepping theorems for convex hulls of finite sets *}
 
 lemma convex_hull_empty[simp]: "convex hull {} = {}"
-  apply(rule hull_unique) by auto
+  by (rule hull_unique) auto
 
 lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
-  apply(rule hull_unique) by auto
+  by (rule hull_unique) auto
 
 lemma convex_hull_insert:
   fixes s :: "'a::real_vector set"
   assumes "s \<noteq> {}"
-  shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
-                                    b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
- apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof-
- fix x assume x:"x = a \<or> x \<in> s"
- thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer
-   apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
+  shows "convex hull (insert a s) =
+    {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
+  (is "?xyz = ?hull")
+  apply (rule, rule hull_minimal, rule)
+  unfolding insert_iff
+  prefer 3
+  apply rule
+proof -
+  fix x
+  assume x: "x = a \<or> x \<in> s"
+  then show "x \<in> ?hull"
+    apply rule
+    unfolding mem_Collect_eq
+    apply (rule_tac x=1 in exI)
+    defer
+    apply (rule_tac x=0 in exI)
+    using assms hull_subset[of s convex]
+    apply auto
+    done
 next
-  fix x assume "x\<in>?hull"
-  then obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto
-  have "a\<in>convex hull insert a s" "b\<in>convex hull insert a s"
-    using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto
-  thus "x\<in> convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def]
-    apply(erule_tac x=a in ballE) apply(erule_tac x=b in ballE) apply(erule_tac x=u in allE) using obt by auto
+  fix x
+  assume "x \<in> ?hull"
+  then obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b"
+    by auto
+  have "a \<in> convex hull insert a s" "b\<in>convex hull insert a s"
+    using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4)
+    by auto
+  then show "x \<in> convex hull insert a s"
+    unfolding obt(5)
+    using convex_convex_hull[of "insert a s", unfolded convex_def]
+    apply (erule_tac x = a in ballE)
+    apply (erule_tac x = b in ballE)
+    apply (erule_tac x = u in allE)
+    using obt apply auto
+    done
 next
-  show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
-    fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
-    from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
-    from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
-    have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
-    have "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
-    proof(cases "u * v1 + v * v2 = 0")
-      have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
-      case True hence **:"u * v1 = 0" "v * v2 = 0"
+  show "convex ?hull"
+    unfolding convex_def
+    apply (rule, rule, rule, rule, rule, rule, rule)
+  proof -
+    fix x y u v
+    assume as: "(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
+    from as(4) obtain u1 v1 b1
+      where obt1: "u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
+    from as(5) obtain u2 v2 b2
+      where obt2: "u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
+    have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
+      by (auto simp add: algebra_simps)
+    have **: "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y =
+      (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
+    proof (cases "u * v1 + v * v2 = 0")
+      case True
+      have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
+        by (auto simp add: algebra_simps)
+      from True have ***: "u * v1 = 0" "v * v2 = 0"
         using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by arith+
-      hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto
-      thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib)
+      then have "u * u1 + v * u2 = 1"
+        using as(3) obt1(3) obt2(3) by auto
+      then show ?thesis
+        unfolding obt1(5) obt2(5) *
+        using assms hull_subset[of s convex]
+        by (auto simp add: *** scaleR_right_distrib)
     next
-      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
-      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
-      also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
-      case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2" apply -
-        apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg)
-        using as(1,2) obt1(1,2) obt2(1,2) by auto
-      thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
-        apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer
-        apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
+      case False
+      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)"
+        using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
+      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)"
+        using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
+      also have "\<dots> = u * v1 + v * v2"
+        by simp
+      finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
+      have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
+        apply (rule add_nonneg_nonneg)
+        prefer 4
+        apply (rule add_nonneg_nonneg)
+        apply (rule_tac [!] mult_nonneg_nonneg)
+        using as(1,2) obt1(1,2) obt2(1,2) apply auto
+        done
+      then show ?thesis
+        unfolding obt1(5) obt2(5)
+        unfolding * and **
+        using False
+        apply (rule_tac x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI)
+        defer
+        apply (rule convex_convex_hull[of s, unfolded convex_def, rule_format])
+        using obt1(4) obt2(4)
         unfolding add_divide_distrib[symmetric] and zero_le_divide_iff
-        by (auto simp add: scaleR_left_distrib scaleR_right_distrib)
-    qed note * = this
-    have u1:"u1 \<le> 1" unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
-    have u2:"u2 \<le> 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
-    have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
-      apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
-    also have "\<dots> \<le> 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
-    finally
-    show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
-      apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
-      using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
+        apply (auto simp add: scaleR_left_distrib scaleR_right_distrib)
+        done
+    qed
+    have u1: "u1 \<le> 1"
+      unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
+    have u2: "u2 \<le> 1"
+      unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
+    have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v"
+      apply (rule add_mono)
+      apply (rule_tac [!] mult_right_mono)
+      using as(1,2) obt1(1,2) obt2(1,2)
+      apply auto
+      done
+    also have "\<dots> \<le> 1"
+      unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
+    finally show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
+      unfolding mem_Collect_eq
+      apply (rule_tac x="u * u1 + v * u2" in exI)
+      apply (rule conjI)
+      defer
+      apply (rule_tac x="1 - u * u1 - v * u2" in exI)
+      unfolding Bex_def
+      using as(1,2) obt1(1,2) obt2(1,2) **
+      apply (auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
+      done
   qed
 qed
 
@@ -1430,162 +1548,307 @@
 
 lemma convex_hull_indexed:
   fixes s :: "'a::real_vector set"
-  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>
-                            (setsum u {1..k} = 1) \<and>
-                            (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
-  apply(rule hull_unique) apply(rule) defer
-  apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
-proof-
-  fix x assume "x\<in>s"
-  thus "x \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
+  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>
+        (setsum u {1..k} = 1) \<and>
+        (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
+  apply (rule hull_unique)
+  apply rule
+  defer
+  apply (subst convex_def)
+  apply (rule, rule, rule, rule, rule, rule, rule)
+proof -
+  fix x
+  assume "x\<in>s"
+  then show "x \<in> ?hull"
+    unfolding mem_Collect_eq
+    apply (rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI)
+    apply auto
+    done
 next
-  fix t assume as:"s \<subseteq> t" "convex t"
-  show "?hull \<subseteq> t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof-
-    fix x k u y assume assm:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
-    show "x\<in>t" unfolding assm(3)[symmetric] apply(rule as(2)[unfolded convex, rule_format])
-      using assm(1,2) as(1) by auto qed
+  fix t
+  assume as: "s \<subseteq> t" "convex t"
+  show "?hull \<subseteq> t"
+    apply rule
+    unfolding mem_Collect_eq
+    apply (erule exE | erule conjE)+
+  proof -
+    fix x k u y
+    assume assm:
+      "\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s"
+      "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
+    show "x\<in>t"
+      unfolding assm(3) [symmetric]
+      apply (rule as(2)[unfolded convex, rule_format])
+      using assm(1,2) as(1) apply auto
+      done
+  qed
 next
-  fix x y u v assume uv:"0\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull"
-  from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto
-  from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto
-  have *:"\<And>P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
+  fix x y u v
+  assume uv: "0\<le>u" "0\<le>v" "u + v = (1::real)" and xy: "x\<in>?hull" "y\<in>?hull"
+  from xy obtain k1 u1 x1 where
+      x: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
+    by auto
+  from xy obtain k2 u2 x2 where
+      y: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
+    by auto
+  have *: "\<And>P (x1::'a) x2 s1 s2 i.
+    (if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
     "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
-    prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)
-  have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto
-  show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)
-    apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
-    apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule)
-    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq
-    unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] proof-
-    fix i assume i:"i \<in> {1..k1+k2}"
-    show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
-    proof(cases "i\<in>{1..k1}")
-      case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto
-    next def j \<equiv> "i - k1"
-      case False with i have "j \<in> {1..k2}" unfolding j_def by auto
-      thus ?thesis unfolding j_def[symmetric] using False
-        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed
-  qed(auto simp add: not_le x(2,3) y(2,3) uv(3))
+    prefer 3
+    apply (rule, rule)
+    unfolding image_iff
+    apply (rule_tac x = "x - k1" in bexI)
+    apply (auto simp add: not_le)
+    done
+  have inj: "inj_on (\<lambda>i. i + k1) {1..k2}"
+    unfolding inj_on_def by auto
+  show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
+    apply rule
+    apply (rule_tac x="k1 + k2" in exI)
+    apply (rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
+    apply (rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI)
+    apply (rule, rule)
+    defer
+    apply rule
+    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and
+      setsum_reindex[OF inj] and o_def Collect_mem_eq
+    unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric]
+  proof -
+    fix i
+    assume i: "i \<in> {1..k1+k2}"
+    show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and>
+      (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
+    proof (cases "i\<in>{1..k1}")
+      case True
+      then show ?thesis
+        using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto
+    next
+      case False
+      def j \<equiv> "i - k1"
+      from i False have "j \<in> {1..k2}" unfolding j_def by auto
+      then show ?thesis
+        unfolding j_def[symmetric]
+        using False
+        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]]
+        apply auto
+        done
+    qed
+  qed (auto simp add: not_le x(2,3) y(2,3) uv(3))
 qed
 
 lemma convex_hull_finite:
   fixes s :: "'a::real_vector set"
   assumes "finite s"
   shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
-         setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
-proof(rule hull_unique, auto simp add: convex_def[of ?set])
-  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"
-    apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
-    unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto
+    setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
+proof (rule hull_unique, auto simp add: convex_def[of ?set])
+  fix x
+  assume "x \<in> s"
+  then show "\<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"
+    apply (rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI)
+    apply auto
+    unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms]
+    apply auto
+    done
 next
-  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
-  fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
-  fix uy assume uy:"\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
-  { fix x assume "x\<in>s"
-    hence "0 \<le> u * ux x + v * uy x" using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
-      by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))  }
-  moreover have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
+  fix u v :: real
+  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+  fix ux assume ux: "\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
+  fix uy assume uy: "\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
+  { fix x
+    assume "x\<in>s"
+    then have "0 \<le> u * ux x + v * uy x"
+      using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
+      apply auto
+      apply (metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))
+      done
+  }
+  moreover
+  have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
     unfolding setsum_addf and setsum_right_distrib[symmetric] and ux(2) uy(2) using uv(3) by auto
-  moreover have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
-    unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] by auto
-  ultimately show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
-    apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto
+  moreover
+  have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
+    unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric]
+    by auto
+  ultimately
+  show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and>
+      (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
+    apply (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI)
+    apply auto
+    done
 next
-  fix t assume t:"s \<subseteq> t" "convex t"
-  fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
-  thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
+  fix t
+  assume t: "s \<subseteq> t" "convex t"
+  fix u
+  assume u: "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
+  then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t"
+    using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
     using assms and t(1) by auto
 qed
 
+
 subsubsection {* Another formulation from Lars Schewe *}
 
 lemma setsum_constant_scaleR:
   fixes y :: "'a::real_vector"
   shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
-apply (cases "finite A")
-apply (induct set: finite)
-apply (simp_all add: algebra_simps)
-done
+  apply (cases "finite A")
+  apply (induct set: finite)
+  apply (simp_all add: algebra_simps)
+  done
 
 lemma convex_hull_explicit:
   fixes p :: "'a::real_vector set"
   shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
-             (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
-proof-
+    (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
+proof -
   { fix x assume "x\<in>?lhs"
-    then obtain k u y where obt:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
+    then obtain k u y where
+        obt: "\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
       unfolding convex_hull_indexed by auto
 
-    have fin:"finite {1..k}" by auto
-    have fin':"\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
-    { fix j assume "j\<in>{1..k}"
-      hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"
-        using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp
-        apply(rule setsum_nonneg) using obt(1) by auto }
+    have fin: "finite {1..k}" by auto
+    have fin': "\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
+    { fix j
+      assume "j\<in>{1..k}"
+      then have "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"
+        using obt(1)[THEN bspec[where x=j]] and obt(2)
+        apply simp
+        apply (rule setsum_nonneg)
+        using obt(1)
+        apply auto
+        done
+    }
     moreover
     have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"
       unfolding setsum_image_gen[OF fin, symmetric] using obt(2) by auto
     moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
       using setsum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
       unfolding scaleR_left.setsum using obt(3) by auto
-    ultimately have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
-      apply(rule_tac x="y ` {1..k}" in exI)
-      apply(rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI) by auto
-    hence "x\<in>?rhs" by auto  }
+    ultimately
+    have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+      apply (rule_tac x="y ` {1..k}" in exI)
+      apply (rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI)
+      apply auto
+      done
+    then have "x\<in>?rhs" by auto
+  }
   moreover
   { fix y assume "y\<in>?rhs"
-    then obtain s u where obt:"finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
-
-    obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
-
-    { fix i::nat assume "i\<in>{1..card s}"
-      hence "f i \<in> s"  apply(subst f(2)[symmetric]) by auto
-      hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto  }
+    then obtain s u where
+      obt: "finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
+
+    obtain f where f: "inj_on f {1..card s}" "f ` {1..card s} = s"
+      using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
+
+    { fix i :: nat
+      assume "i\<in>{1..card s}"
+      then have "f i \<in> s"
+        apply (subst f(2)[symmetric])
+        apply auto
+        done
+      then have "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto
+    }
     moreover have *:"finite {1..card s}" by auto
-    { fix y assume "y\<in>s"
-      then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto
-      hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto
-      hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
-      hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
-            "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
-        by (auto simp add: setsum_constant_scaleR)   }
-
-    hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
+    { fix y
+      assume "y\<in>s"
+      then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"]
+        by auto
+      then have "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}"
+        apply auto
+        using f(1)[unfolded inj_on_def]
+        apply(erule_tac x=x in ballE)
+        apply auto
+        done
+      then have "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
+      then have "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
+          "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
+        by (auto simp add: setsum_constant_scaleR)
+    }
+    then have "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
       unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
       unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
-      using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto
-
-    ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
-      apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastforce
-    hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto  }
+      using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u]
+      unfolding obt(4,5) by auto
+    ultimately
+    have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and>
+        (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
+      apply (rule_tac x="card s" in exI)
+      apply (rule_tac x="u \<circ> f" in exI)
+      apply (rule_tac x=f in exI)
+      apply fastforce
+      done
+    then have "y \<in> ?lhs" unfolding convex_hull_indexed by auto
+  }
   ultimately show ?thesis unfolding set_eq_iff by blast
 qed
 
+
 subsubsection {* A stepping theorem for that expansion *}
 
 lemma convex_hull_finite_step:
-  fixes s :: "'a::real_vector set" assumes "finite s"
+  fixes s :: "'a::real_vector set"
+  assumes "finite s"
   shows "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)
      \<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs")
-proof(rule, case_tac[!] "a\<in>s")
-  assume "a\<in>s" hence *:"insert a s = s" by auto
-  assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto
+proof (rule, case_tac[!] "a\<in>s")
+  assume "a\<in>s"
+  then have *:" insert a s = s" by auto
+  assume ?lhs
+  then show ?rhs
+    unfolding *
+    apply (rule_tac x=0 in exI)
+    apply auto
+    done
 next
-  assume ?lhs then obtain u where u:"\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto
-  assume "a\<notin>s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp
-    apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s` by auto
+  assume ?lhs
+  then obtain u where u: "\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y"
+    by auto
+  assume "a \<notin> s"
+  then show ?rhs
+    apply (rule_tac x="u a" in exI)
+    using u(1)[THEN bspec[where x=a]]
+    apply simp
+    apply (rule_tac x=u in exI)
+    using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s`
+    apply auto
+    done
 next
-  assume "a\<in>s" hence *:"insert a s = s" by auto
-  have fin:"finite (insert a s)" using assms by auto
-  assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
-  show ?lhs apply(rule_tac x="\<lambda>x. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin]
-    unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s` by auto
+  assume "a \<in> s"
+  then have *: "insert a s = s" by auto
+  have fin: "finite (insert a s)" using assms by auto
+  assume ?rhs
+  then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+    by auto
+  show ?lhs
+    apply (rule_tac x = "\<lambda>x. (if a = x then v else 0) + u x" in exI)
+    unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin]
+    unfolding setsum_clauses(2)[OF assms]
+    using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s`
+    apply auto
+    done
 next
-  assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
-  moreover assume "a\<notin>s" moreover have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
-    apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\<notin>s` by auto
-  ultimately show ?lhs apply(rule_tac x="\<lambda>x. if a = x then v else u x" in exI)  unfolding setsum_clauses(2)[OF assms] by auto
-qed
+  assume ?rhs
+  then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+    by auto
+  moreover
+  assume "a \<notin> s"
+  moreover
+  have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
+    apply (rule_tac setsum_cong2)
+    defer
+    apply (rule_tac setsum_cong2)
+    using `a \<notin> s`
+    apply auto
+    done
+  ultimately show ?lhs
+    apply (rule_tac x="\<lambda>x. if a = x then v else u x" in exI)
+    unfolding setsum_clauses(2)[OF assms]
+    apply auto
+    done
+qed
+
 
 subsubsection {* Hence some special cases *}