# HG changeset patch
# User wenzelm
# Date 1384721172 -3600
# Node ID 2f7867850cc3005736ba561d0aff447c25d3e872
# Parent  b0074321bf1418726d3c835ffcd5759a6b4c622a
tuned proofs;

diff -r b0074321bf14 -r 2f7867850cc3 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Nov 17 20:24:37 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Nov 17 21:46:12 2013 +0100
@@ -277,13 +277,13 @@
   assumes "linear f" "inj f"
   shows "f ` (closure S) = closure (f ` S)"
 proof -
-  obtain f' where f'_def: "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
+  obtain f' where f': "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
     using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
   then have "f' ` closure (f ` S) \<le> closure (S)"
     using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
   then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto
   then have "closure (f ` S) \<le> f ` closure S"
-    using image_compose[of f f' "closure (f ` S)"] f'_def by auto
+    using image_compose[of f f' "closure (f ` S)"] f' by auto
   then show ?thesis using closure_linear_image[of f S] assms by auto
 qed
 
@@ -304,7 +304,7 @@
 lemma snd_linear: "linear snd"
   unfolding linear_iff by (simp add: algebra_simps)
 
-lemma fst_snd_linear: "linear (%(x,y). x + y)"
+lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
   unfolding linear_iff by (simp add: algebra_simps)
 
 lemma scaleR_2:
@@ -938,18 +938,19 @@
     assume assm: "affine S \<and> 0 \<in> S"
     {
       fix c :: real
-      fix x assume x_def: "x \<in> S"
+      fix x
+      assume x: "x \<in> S"
       have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
       moreover
       have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S"
-        using affine_alt[of S] assm x_def by auto
+        using affine_alt[of S] assm x by auto
       ultimately have "c *\<^sub>R x \<in> S" by auto
     }
     then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto
 
     {
       fix x y
-      assume xy_def: "x \<in> S" "y \<in> S"
+      assume xy: "x \<in> S" "y \<in> S"
       def u == "(1 :: real)/2"
       have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)"
         by auto
@@ -957,16 +958,16 @@
       have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y"
         by (simp add: algebra_simps)
       moreover
-      have "(1-u) *\<^sub>R x + u *\<^sub>R y \<in> S"
-        using affine_alt[of S] assm xy_def by auto
+      have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S"
+        using affine_alt[of S] assm xy by auto
       ultimately
       have "(1/2) *\<^sub>R (x+y) \<in> S"
         using u_def by auto
       moreover
-      have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))"
+      have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))"
         by auto
       ultimately
-      have "(x+y) \<in> S"
+      have "x + y \<in> S"
         using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
     }
     then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S"
@@ -990,13 +991,14 @@
 qed
 
 lemma parallel_subspace_explicit:
-  assumes "affine S" "a : S"
-  assumes "L \<equiv> {y. \<exists>x \<in> S. (-a)+x=y}"
-  shows "subspace L & affine_parallel S L"
+  assumes "affine S"
+    and "a \<in> S"
+  assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}"
+  shows "subspace L \<and> affine_parallel S L"
 proof -
   from assms have "L = plus (- a) ` S" by auto
   then have par: "affine_parallel S L"
-    unfolding affine_parallel_def .. 
+    unfolding affine_parallel_def ..
   then have "affine L" using assms parallel_is_affine by auto
   moreover have "0 \<in> L"
     using assms by auto
@@ -1010,14 +1012,14 @@
     and "affine_parallel A B"
   shows "A \<supseteq> B"
 proof -
-  from assms obtain a where a_def: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
+  from assms obtain a where a: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
     using affine_parallel_expl[of A B] by auto
   then have "-a \<in> A"
     using assms subspace_0[of B] by auto
   then have "a \<in> A"
     using assms subspace_neg[of A "-a"] by auto
   then show ?thesis
-    using assms a_def unfolding subspace_def by auto
+    using assms a unfolding subspace_def by auto
 qed
 
 lemma parallel_subspace:
@@ -1116,7 +1118,7 @@
         then have "x \<in> (op *\<^sub>R c) ` S"
           unfolding image_def
           using `cone S` `c>0` mem_cone[of S x "1/c"]
-            exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
+            exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
           by auto
       }
       moreover
@@ -1169,17 +1171,17 @@
   {
     fix x
     assume "x \<in> ?rhs"
-    then obtain cx :: real and xx where x_def: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
+    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
       by auto
     fix c :: real
     assume c: "c \<ge> 0"
     then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
-      using x_def by (simp add: algebra_simps)
+      using x by (simp add: algebra_simps)
     moreover
     have "c * cx \<ge> 0"
-      using c x_def using mult_nonneg_nonneg by auto
+      using c x using mult_nonneg_nonneg by auto
     ultimately
-    have "c *\<^sub>R x \<in> ?rhs" using x_def by auto
+    have "c *\<^sub>R x \<in> ?rhs" using x by auto
   }
   then have "cone ?rhs"
     unfolding cone_def by auto
@@ -1202,12 +1204,12 @@
   {
     fix x
     assume "x \<in> ?rhs"
-    then obtain cx :: real and xx where x_def: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
+    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
       by auto
     then have "xx \<in> cone hull S"
       using hull_subset[of S] by auto
     then have "x \<in> ?lhs"
-      using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
+      using x cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
   }
   ultimately show ?thesis by auto
 qed
@@ -2398,27 +2400,27 @@
     by (metis hull_minimal)
   then have "affine hull ((\<lambda>x. a + x) ` S) >= (\<lambda>x. a + x) ` (affine hull S)"
     by auto
-  from this show ?thesis using h1 by auto
+  then show ?thesis using h1 by auto
 qed
 
 lemma affine_dependent_translation:
   assumes "affine_dependent S"
   shows "affine_dependent ((\<lambda>x. a + x) ` S)"
 proof -
-  obtain x where x_def: "x \<in> S \<and> x \<in> affine hull (S - {x})"
+  obtain x where x: "x \<in> S \<and> x \<in> affine hull (S - {x})"
     using assms affine_dependent_def by auto
   have "op + a ` (S - {x}) = op + a ` S - {a + x}"
     by auto
   then have "a + x \<in> affine hull ((\<lambda>x. a + x) ` S - {a + x})"
-    using affine_hull_translation[of a "S - {x}"] x_def by auto
+    using affine_hull_translation[of a "S - {x}"] x by auto
   moreover have "a + x \<in> (\<lambda>x. a + x) ` S"
-    using x_def by auto
+    using x by auto
   ultimately show ?thesis
     unfolding affine_dependent_def by auto
 qed
 
 lemma affine_dependent_translation_eq:
-  "affine_dependent S <-> affine_dependent ((\<lambda>x. a + x) ` S)"
+  "affine_dependent S \<longleftrightarrow> affine_dependent ((\<lambda>x. a + x) ` S)"
 proof -
   {
     assume "affine_dependent ((\<lambda>x. a + x) ` S)"
@@ -2434,12 +2436,12 @@
   assumes "0 \<in> affine hull S"
   shows "dependent S"
 proof -
-  obtain s u where s_u_def: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
+  obtain s u where s_u: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
     using assms affine_hull_explicit[of S] by auto
   then have "\<exists>v\<in>s. u v \<noteq> 0"
     using setsum_not_0[of "u" "s"] by auto
   then have "finite s \<and> s \<subseteq> S \<and> (\<exists>v\<in>s. u v \<noteq> 0 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0)"
-    using s_u_def by auto
+    using s_u by auto
   then show ?thesis
     unfolding dependent_explicit[of S] by auto
 qed
@@ -2448,7 +2450,7 @@
   assumes "affine_dependent (insert 0 S)"
   shows "dependent S"
 proof -
-  obtain x where x_def: "x \<in> insert 0 S \<and> x \<in> affine hull (insert 0 S - {x})"
+  obtain x where x: "x \<in> insert 0 S \<and> x \<in> affine hull (insert 0 S - {x})"
     using affine_dependent_def[of "(insert 0 S)"] assms by blast
   then have "x \<in> span (insert 0 S - {x})"
     using affine_hull_subset_span by auto
@@ -2456,12 +2458,12 @@
     using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto
   ultimately have "x \<in> span (S - {x})" by auto
   then have "x \<noteq> 0 \<Longrightarrow> dependent S"
-    using x_def dependent_def by auto
+    using x dependent_def by auto
   moreover
   {
     assume "x = 0"
     then have "0 \<in> affine hull S"
-      using x_def hull_mono[of "S - {0}" S] by auto
+      using x hull_mono[of "S - {0}" S] by auto
     then have "dependent S"
       using affine_hull_0_dependent by auto
   }
@@ -2549,11 +2551,11 @@
   assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}"
   shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
 proof -
-  obtain a where a_def: "a \<in> S"
+  obtain a where a: "a \<in> S"
     using assms by auto
   then have h0: "independent  ((\<lambda>x. -a + x) ` (S-{a}))"
     using affine_dependent_iff_dependent2 assms by auto
-  then obtain B where B_def:
+  then obtain B where B:
     "(\<lambda>x. -a+x) ` (S - {a}) \<subseteq> B \<and> B \<subseteq> (\<lambda>x. -a+x) ` V \<and> independent B \<and> (\<lambda>x. -a+x) ` V \<subseteq> span B"
      using maximal_independent_subset_extend[of "(\<lambda>x. -a+x) ` (S-{a})" "(\<lambda>x. -a + x) ` V"] assms
      by blast
@@ -2564,18 +2566,18 @@
     using affine_hull_insert_span_gen[of a "((\<lambda>x. a+x) ` B)"] translation_assoc[of "-a" a B]
     by auto
   then have "V \<subseteq> affine hull T"
-    using B_def assms translation_inverse_subset[of a V "span B"]
+    using B assms translation_inverse_subset[of a V "span B"]
     by auto
   moreover have "T \<subseteq> V"
-    using T_def B_def a_def assms by auto
+    using T_def B a assms by auto
   ultimately have "affine hull T = affine hull V"
     by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
   moreover have "S \<subseteq> T"
-    using T_def B_def translation_inverse_subset[of a "S-{a}" B]
+    using T_def B translation_inverse_subset[of a "S-{a}" B]
     by auto
   moreover have "\<not> affine_dependent T"
     using T_def affine_dependent_translation_eq[of "insert 0 B"]
-      affine_dependent_imp_dependent2 B_def
+      affine_dependent_imp_dependent2 B
     by auto
   ultimately show ?thesis using `T \<subseteq> V` by auto
 qed
@@ -2670,31 +2672,31 @@
   shows "aff_dim V = int (dim L)"
 proof -
   obtain B where
-    B_def: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1"
+    B: "affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> int (card B) = aff_dim V + 1"
     using aff_dim_basis_exists by auto
   then have "B \<noteq> {}"
-    using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B]
+    using assms B affine_hull_nonempty[of V] affine_hull_nonempty[of B]
     by auto
-  then obtain a where a_def: "a \<in> B" by auto
+  then obtain a where a: "a \<in> B" by auto
   def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))"
   moreover have "affine_parallel (affine hull B) Lb"
-    using Lb_def B_def assms affine_hull_span2[of a B] a_def
+    using Lb_def B assms affine_hull_span2[of a B] a
       affine_parallel_commut[of "Lb" "(affine hull B)"]
     unfolding affine_parallel_def
     by auto
   moreover have "subspace Lb"
     using Lb_def subspace_span by auto
   moreover have "affine hull B \<noteq> {}"
-    using assms B_def affine_hull_nonempty[of V] by auto
+    using assms B affine_hull_nonempty[of V] by auto
   ultimately have "L = Lb"
-    using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def
+    using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B
     by auto
   then have "dim L = dim Lb"
     by auto
   moreover have "card B - 1 = dim Lb" and "finite B"
-    using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto
+    using Lb_def aff_dim_parallel_subspace_aux a B by auto
   ultimately show ?thesis
-    using B_def `B \<noteq> {}` card_gt_0_iff[of B] by auto
+    using B `B \<noteq> {}` card_gt_0_iff[of B] by auto
 qed
 
 lemma aff_independent_finite:
@@ -2782,7 +2784,7 @@
     defer
     unfolding dim_span[of B]
     apply(rule B)
-    unfolding span_substd_basis[OF d, symmetric] 
+    unfolding span_substd_basis[OF d, symmetric]
     apply (rule span_inc)
     apply (rule independent_substdbasis[OF d])
     apply rule
@@ -2831,10 +2833,10 @@
     using `B = {}` by auto
 next
   case False
-  then obtain a where a_def: "a \<in> B" by auto
+  then obtain a where a: "a \<in> B" by auto
   def Lb \<equiv> "span ((\<lambda>x. -a+x) ` (B-{a}))"
   have "affine_parallel (affine hull B) Lb"
-    using Lb_def affine_hull_span2[of a B] a_def
+    using Lb_def affine_hull_span2[of a B] a
       affine_parallel_commut[of "Lb" "(affine hull B)"]
     unfolding affine_parallel_def by auto
   moreover have "subspace Lb"
@@ -2842,7 +2844,7 @@
   ultimately have "aff_dim B = int(dim Lb)"
     using aff_dim_parallel_subspace[of B Lb] `B \<noteq> {}` by auto
   moreover have "(card B) - 1 = dim Lb" "finite B"
-    using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto
+    using Lb_def aff_dim_parallel_subspace_aux a assms by auto
   ultimately have "of_nat (card B) = aff_dim B + 1"
     using `B \<noteq> {}` card_gt_0_iff[of B] by auto
   then show ?thesis
@@ -3171,8 +3173,8 @@
   assume *: "x \<in> S" "open T" "x \<in> T" "T \<inter> affine hull S \<subseteq> S"
   then have **: "x \<in> T \<inter> affine hull S"
     using hull_inc by auto
-  show "\<exists>Tb. (\<exists>Ta. open Ta \<and> Tb = affine hull S Int Ta) \<and> x \<in> Tb \<and> Tb \<subseteq> S"
-    apply (rule_tac x="T Int (affine hull S)" in exI)
+  show "\<exists>Tb. (\<exists>Ta. open Ta \<and> Tb = affine hull S \<inter> Ta) \<and> x \<in> Tb \<and> Tb \<subseteq> S"
+    apply (rule_tac x = "T \<inter> (affine hull S)" in exI)
     using * **
     apply auto
     done
@@ -3287,7 +3289,7 @@
     and "e \<le> 1"
   shows "x - e *\<^sub>R (x - c) \<in> rel_interior S"
 proof -
-  obtain d where "d > 0" and d: "ball c d Int affine hull S \<subseteq> S"
+  obtain d where "d > 0" and d: "ball c d \<inter> affine hull S \<subseteq> S"
     using assms(2) unfolding  mem_rel_interior_ball by auto
   {
     fix y
@@ -3657,7 +3659,7 @@
   {
     fix x
     assume x: "x \<in> rel_interior S"
-    then obtain e2 where e2: "e2 > 0" "cball x e2 Int affine hull S \<subseteq> S"
+    then obtain e2 where e2: "e2 > 0" "cball x e2 \<inter> affine hull S \<subseteq> S"
       using rel_interior_cball[of S] by auto
     have "x \<in> S" using x rel_interior_subset by auto
     then have *: "f x \<in> f ` S" by auto
@@ -3786,7 +3788,7 @@
       moreover from `x\<in>t` have "x \<in> s"
         using obt(2) by auto
       ultimately have "x + (y - a) \<in> s"
-        using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast 
+        using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast
     }
     moreover
     have *: "inj_on (\<lambda>v. v + (y - a)) t"
@@ -4756,7 +4758,8 @@
   then show ?thesis by auto
 next
   case False
-  then have *: "0 \<in> S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto
+  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)"
+    using cone_iff[of S] assms by auto
   {
     fix c :: real
     assume "c > 0"
@@ -4784,7 +4787,7 @@
   unfolding Inter_iff Ball_def mem_Collect_eq
   apply (rule,rule,erule conjE)
 proof -
-  fix x 
+  fix x
   assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. inner a x \<le> b}) \<longrightarrow> x \<in> xa"
   then have "\<forall>a b. s \<subseteq> {x. inner a x \<le> b} \<longrightarrow> x \<in> {x. inner a x \<le> b}"
     by blast
@@ -5675,28 +5678,55 @@
   "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
   unfolding is_interval_def by auto
 
-lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::real set)"
-  apply(rule, rule is_interval_connected, assumption) unfolding is_interval_1
-  apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof-
-  fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x\<notin>s"
-  hence *:"a < x" "x < b" unfolding not_le [symmetric] by auto
-  let ?halfl = "{..<x} " and ?halfr = "{x<..} "
-  { fix y assume "y \<in> s" with `x \<notin> s` have "x \<noteq> y" by auto
-    then have "y \<in> ?halfr \<union> ?halfl" by auto }
-  moreover have "a\<in>?halfl" "b\<in>?halfr" using * by auto
-  hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}"  using as(2-3) by auto
-  ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
-    apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI)
-    apply(rule, rule open_lessThan, rule, rule open_greaterThan)
-    by auto qed
+lemma is_interval_connected_1:
+  fixes s :: "real set"
+  shows "is_interval s \<longleftrightarrow> connected s"
+  apply rule
+  apply (rule is_interval_connected, assumption)
+  unfolding is_interval_1
+  apply rule
+  apply rule
+  apply rule
+  apply rule
+  apply (erule conjE)
+  apply (rule ccontr)
+proof -
+  fix a b x
+  assume as: "connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x \<notin> s"
+  then have *: "a < x" "x < b"
+    unfolding not_le [symmetric] by auto
+  let ?halfl = "{..<x} "
+  let ?halfr = "{x<..}"
+  {
+    fix y
+    assume "y \<in> s"
+    with `x \<notin> s` have "x \<noteq> y" by auto
+    then have "y \<in> ?halfr \<union> ?halfl" by auto
+  }
+  moreover have "a \<in> ?halfl" "b \<in> ?halfr" using * by auto
+  then have "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}"
+    using as(2-3) by auto
+  ultimately show False
+    apply (rule_tac notE[OF as(1)[unfolded connected_def]])
+    apply (rule_tac x = ?halfl in exI)
+    apply (rule_tac x = ?halfr in exI)
+    apply rule
+    apply (rule open_lessThan)
+    apply rule
+    apply (rule open_greaterThan)
+    apply auto
+    done
+qed
 
 lemma is_interval_convex_1:
-  "is_interval s \<longleftrightarrow> convex (s::real set)"
-by(metis is_interval_convex convex_connected is_interval_connected_1)
+  fixes s :: "real set"
+  shows "is_interval s \<longleftrightarrow> convex s"
+  by (metis is_interval_convex convex_connected is_interval_connected_1)
 
 lemma convex_connected_1:
-  "connected s \<longleftrightarrow> convex (s::real set)"
-by(metis is_interval_convex convex_connected is_interval_connected_1)
+  fixes s :: "real set"
+  shows "connected s \<longleftrightarrow> convex s"
+  by (metis is_interval_convex convex_connected is_interval_connected_1)
 
 
 subsection {* Another intermediate value theorem formulation *}
@@ -6604,7 +6634,7 @@
 lemma substd_simplex:
   assumes d: "d \<subseteq> Basis"
   shows "convex hull (insert 0 d) =
-    {x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d --> x\<bullet>i = 0)}"
+    {x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)}"
   (is "convex hull (insert 0 ?p) = ?s")
 proof -
   let ?D = d
@@ -6613,7 +6643,7 @@
   from d have "finite d"
     by (blast intro: finite_subset finite_Basis)
   show ?thesis
-    unfolding simplex[OF `finite d` `0 ~: ?p`]
+    unfolding simplex[OF `finite d` `0 \<notin> ?p`]
     apply (rule set_eqI)
     unfolding mem_Collect_eq
     apply rule
@@ -6624,7 +6654,7 @@
     fix u
     assume as: "\<forall>x\<in>?D. 0 \<le> u x" "setsum u ?D \<le> 1" "(\<Sum>x\<in>?D. u x *\<^sub>R x) = x"
     have *: "\<forall>i\<in>Basis. i:d \<longrightarrow> u i = x\<bullet>i"
-      and "(\<forall>i\<in>Basis. i ~: d --> x \<bullet> i = 0)"
+      and "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)"
       using as(3)
       unfolding substdbasis_expansion_unique[OF assms]
       by auto
@@ -6838,8 +6868,9 @@
         unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
       have x0: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)"
         using x rel_interior_subset  substd_simplex[OF assms] by auto
-      have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> setsum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d --> x\<bullet>i = 0)"
-        apply (rule, rule)
+      have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> setsum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)"
+        apply rule
+        apply rule
       proof -
         fix i :: 'a
         assume "i \<in> d"
@@ -6891,7 +6922,7 @@
         by auto
       moreover have "\<forall>i. i \<in> d \<or> i \<notin> d" by auto
       ultimately
-      have "\<forall>i. (\<forall>i\<in>d. 0 < x\<bullet>i) \<and> (\<forall>i. i \<notin> d \<longrightarrow> x\<bullet>i = 0) --> 0 \<le> x\<bullet>i"
+      have "\<forall>i. (\<forall>i\<in>d. 0 < x\<bullet>i) \<and> (\<forall>i. i \<notin> d \<longrightarrow> x\<bullet>i = 0) \<longrightarrow> 0 \<le> x\<bullet>i"
         by metis
       then have h2: "x \<in> convex hull (insert 0 ?p)"
         using as assms
@@ -6908,7 +6939,7 @@
         using as using `0 < card d` by auto
       ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0"
         by auto
-    
+
       have "x \<in> rel_interior (convex hull (insert 0 ?p))"
         unfolding rel_interior_ball mem_Collect_eq h0
         apply (rule,rule h2)
@@ -6940,7 +6971,7 @@
           using `0 < card d`
           by auto
         finally show "setsum (op \<bullet> y) d \<le> 1" .
-    
+
         fix i :: 'a
         assume i: "i \<in> Basis"
         then show "0 \<le> y\<bullet>i"
@@ -7280,7 +7311,7 @@
   moreover
   {
     fix z
-    assume z: "z : rel_interior (closure S)"
+    assume z: "z \<in> rel_interior (closure S)"
     obtain x where x: "x \<in> rel_interior S"
       using `S \<noteq> {}` assms rel_interior_convex_nonempty by auto
     have "z \<in> rel_interior S"
@@ -7289,7 +7320,7 @@
       then show ?thesis using x by auto
     next
       case False
-      obtain e where e: "e > 0" "cball z e Int affine hull closure S \<le> closure S"
+      obtain e where e: "e > 0" "cball z e \<inter> affine hull closure S \<le> closure S"
         using z rel_interior_cball[of "closure S"] by auto
       then have *: "0 < e/norm(z-x)"
         using e False divide_pos_pos[of e "norm(z-x)"] by auto
@@ -7338,7 +7369,7 @@
   assumes "convex S1"
     and "convex S2"
   shows "closure S1 = closure S2 \<longleftrightarrow> rel_interior S1 \<le> S2 \<and> S2 \<subseteq> closure S1"
-  (is "?A <-> ?B")
+  (is "?A \<longleftrightarrow> ?B")
 proof
   assume ?A
   then show ?B
@@ -7422,7 +7453,7 @@
        using mem_rel_interior[of a S1] a by auto
     then have "a \<in> T \<inter> closure S2"
       using a assms unfolding rel_frontier_def by auto
-    then obtain b where b: "b \<in> T Int rel_interior S2"
+    then obtain b where b: "b \<in> T \<inter> rel_interior S2"
       using open_inter_closure_rel_interior[of S2 T] assms T by auto
     then have "b \<in> affine hull S1"
       using rel_interior_subset hull_subset[of S2] ** by auto
@@ -7442,12 +7473,13 @@
     and "z \<in> rel_interior S"
   shows "\<forall>x\<in>affine hull S. \<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)"
 proof -
-  obtain e1 where e1: "e1>0 & cball z e1 Int affine hull S <= S"
-      using mem_rel_interior_cball[of z S] assms by auto
+  obtain e1 where e1: "e1 > 0 \<and> cball z e1 \<inter> affine hull S \<subseteq> S"
+    using mem_rel_interior_cball[of z S] assms by auto
   {
     fix x
     assume x: "x \<in> affine hull S"
-    { assume "x ~= z"
+    {
+      assume "x \<noteq> z"
       def m \<equiv> "1 + e1/norm(x-z)"
       then have "m > 1"
         using e1 `x \<noteq> z` divide_pos_pos[of e1 "norm (x - z)"] by auto
@@ -7568,18 +7600,18 @@
     assume r: "\<forall>x. \<exists>e. e > 0 \<and> z + e *\<^sub>R x \<in> S"
     {
       fix x
-      obtain e1 where e1_def: "e1 > 0 \<and> z + e1 *\<^sub>R (x - z) \<in> S"
+      obtain e1 where e1: "e1 > 0 \<and> z + e1 *\<^sub>R (x - z) \<in> S"
         using r by auto
-      obtain e2 where e2_def: "e2 > 0 \<and> z + e2 *\<^sub>R (z - x) \<in> S"
+      obtain e2 where e2: "e2 > 0 \<and> z + e2 *\<^sub>R (z - x) \<in> S"
         using r by auto
       def x1 \<equiv> "z + e1 *\<^sub>R (x - z)"
       then have x1: "x1 \<in> affine hull S"
-        using e1_def hull_subset[of S] by auto
+        using e1 hull_subset[of S] by auto
       def x2 \<equiv> "z + e2 *\<^sub>R (z - x)"
       then have x2: "x2 \<in> affine hull S"
-        using e2_def hull_subset[of S] by auto
+        using e2 hull_subset[of S] by auto
       have *: "e1/(e1+e2) + e2/(e1+e2) = 1"
-        using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp
+        using add_divide_distrib[of e1 e2 "e1+e2"] e1 e2 by simp
       then have "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
         using x1_def x2_def
         apply (auto simp add: algebra_simps)
@@ -7593,7 +7625,7 @@
       have "x1 - x2 = (e1 + e2) *\<^sub>R (x - z)"
         using x1_def x2_def by (auto simp add: algebra_simps)
       then have "x = z+(1/(e1+e2)) *\<^sub>R (x1-x2)"
-        using e1_def e2_def by simp
+        using e1 e2 by simp
       then have "x \<in> affine hull S"
         using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"]
           x1 x2 z affine_affine_hull[of S]
@@ -7690,9 +7722,9 @@
   }
   then have "\<Inter>I \<subseteq> \<Inter>{closure S |S. S \<in> I}"
     by auto
-  moreover have "closed (Inter {closure S |S. S \<in> I})"
+  moreover have "closed (\<Inter>{closure S |S. S \<in> I})"
     unfolding closed_Inter closed_closure by auto
-  ultimately show ?thesis using closure_hull[of "Inter I"]
+  ultimately show ?thesis using closure_hull[of "\<Inter>I"]
     hull_minimal[of "\<Inter>I" "\<Inter>{closure S |S. S \<in> I}" "closed"] by auto
 qed
 
@@ -7711,7 +7743,7 @@
     {
       assume "y = x"
       then have "y \<in> closure (\<Inter>{rel_interior S |S. S \<in> I})"
-        using x closure_subset[of "Inter {rel_interior S |S. S \<in> I}"] by auto
+        using x closure_subset[of "\<Inter>{rel_interior S |S. S \<in> I}"] by auto
     }
     moreover
     {
@@ -7753,13 +7785,13 @@
 lemma convex_closure_inter:
   assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
     and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-  shows "closure (Inter I) = Inter {closure S |S. S \<in> I}"
+  shows "closure (\<Inter>I) = \<Inter>{closure S |S. S \<in> I}"
 proof -
   have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
     using convex_closure_rel_interior_inter assms by auto
   moreover
-  have "closure (Inter {rel_interior S |S. S \<in> I}) \<le> closure (Inter I)"
-    using rel_interior_inter_aux closure_mono[of "Inter {rel_interior S |S. S \<in> I}" "\<Inter>I"]
+  have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter> I)"
+    using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
     by auto
   ultimately show ?thesis
     using closure_inter[of I] by auto
@@ -7768,13 +7800,13 @@
 lemma convex_inter_rel_interior_same_closure:
   assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
     and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-  shows "closure (Inter {rel_interior S |S. S \<in> I}) = closure (\<Inter>I)"
+  shows "closure (\<Inter>{rel_interior S |S. S \<in> I}) = closure (\<Inter>I)"
 proof -
   have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
     using convex_closure_rel_interior_inter assms by auto
   moreover
   have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
-    using rel_interior_inter_aux closure_mono[of "Inter {rel_interior S |S. S \<in> I}" "\<Inter>I"]
+    using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
     by auto
   ultimately show ?thesis
     using closure_inter[of I] by auto
@@ -7783,12 +7815,12 @@
 lemma convex_rel_interior_inter:
   assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
     and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
-  shows "rel_interior (Inter I) \<le> Inter {rel_interior S |S. S \<in> I}"
+  shows "rel_interior (\<Inter>I) \<subseteq> \<Inter>{rel_interior S |S. S \<in> I}"
 proof -
   have "convex (\<Inter>I)"
     using assms convex_Inter by auto
   moreover
-  have "convex(Inter {rel_interior S |S. S \<in> I})"
+  have "convex (\<Inter>{rel_interior S |S. S \<in> I})"
     apply (rule convex_Inter)
     using assms convex_rel_interior
     apply auto
@@ -7968,18 +8000,18 @@
       fix x
       assume "x \<in> f ` S"
       then obtain x1 where x1: "x1 \<in> S" "f x1 = x" by auto
-      then obtain e where e_def: "e > 1" "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1 : S"
+      then obtain e where e: "e > 1" "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1 : S"
         using convex_rel_interior_iff[of S z1] `convex S` x1 z1 by auto
       moreover have "f ((1 - e) *\<^sub>R x1 + e *\<^sub>R z1) = (1 - e) *\<^sub>R x + e *\<^sub>R z"
         using x1 z1 `linear f` by (simp add: linear_add_cmul)
       ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S"
         using imageI[of "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1" S f] by auto
       then have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S"
-        using e_def by auto
+        using e by auto
     }
     then have "z \<in> rel_interior (f ` S)"
       using convex_rel_interior_iff[of "f ` S" z] `convex S`
-        `linear f` `S ~= {}` convex_linear_image[of f S]  linear_conv_bounded_linear[of f]
+        `linear f` `S \<noteq> {}` convex_linear_image[of f S]  linear_conv_bounded_linear[of f]
       by auto
   }
   ultimately show ?thesis by auto
@@ -8022,7 +8054,7 @@
       using convex_rel_interior_iff[of "f -` S" z] conv nonemp by auto
   }
   moreover
-  { 
+  {
     fix z
     assume z: "z \<in> rel_interior (f -` S)"
     {
@@ -8037,7 +8069,7 @@
         using e by auto
     }
     then have "f z \<in> rel_interior (S \<inter> range f)"
-      using `convex (S Int (range f))` `S \<inter> range f \<noteq> {}`
+      using `convex (S \<inter> (range f))` `S \<inter> range f \<noteq> {}`
         convex_rel_interior_iff[of "S \<inter> (range f)" "f z"]
       by auto
     moreover have "affine (range f)"
@@ -8132,7 +8164,7 @@
   assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set) \<and> rel_open S"
     and "finite I"
   shows "convex (\<Inter>I) \<and> rel_open (\<Inter>I)"
-proof (cases "Inter {rel_interior S |S. S : I} = {}")
+proof (cases "\<Inter>{rel_interior S |S. S \<in> I} = {}")
   case True
   then have "\<Inter>I = {}"
     using assms unfolding rel_open_def by auto
@@ -8140,7 +8172,7 @@
     unfolding rel_open_def using rel_interior_empty by auto
 next
   case False
-  then have "rel_open (Inter I)"
+  then have "rel_open (\<Inter>I)"
     using assms unfolding rel_open_def
     using convex_rel_interior_finite_inter[of I]
     by auto
@@ -8290,191 +8322,274 @@
   then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)"
     using cone_iff[of S] assms by auto
   then have *: "0 \<in> ({0} \<union> rel_interior S)"
-    and "\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` ({0} \<union> rel_interior S) = ({0} Un rel_interior S)"
+    and "\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
     by (auto simp add: rel_interior_scaleR)
   then show ?thesis
-    using cone_iff[of "{0} Un rel_interior S"] by auto
+    using cone_iff[of "{0} \<union> rel_interior S"] by auto
 qed
 
 lemma rel_interior_convex_cone_aux:
-fixes S :: "('m::euclidean_space) set"
-assumes "convex S"
-shows "(c,x) : rel_interior (cone hull ({(1 :: real)} <*> S)) <->
-       c>0 & x : ((op *\<^sub>R c) ` (rel_interior S))"
-proof-
-{ assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) }
-moreover
-{ assume "S ~= {}" from this obtain s where "s : S" by auto
-have conv: "convex ({(1 :: real)} <*> S)" using convex_Times[of "{(1 :: real)}" S]
-   assms convex_singleton[of "1 :: real"] by auto
-def f == "(%y. {z. (y,z) : cone hull ({(1 :: real)} <*> S)})"
-hence *: "(c, x) : rel_interior (cone hull ({(1 :: real)} <*> S)) =
-      (c : rel_interior {y. f y ~= {}} & x : 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 by auto
-{ fix y assume "(y :: real)>=0"
-  hence "y *\<^sub>R (1,s) : cone hull ({(1 :: real)} <*> S)"
-     using cone_hull_expl[of "{(1 :: real)} <*> S"] `s:S` by auto
-  hence "f y ~= {}" using f_def by auto
-}
-hence "{y. f y ~= {}} = {0..}" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto
-hence **: "rel_interior {y. f y ~= {}} = {0<..}" using rel_interior_real_semiline by auto
-{ fix c assume "c>(0 :: real)"
-  hence "f c = (op *\<^sub>R c ` S)" using f_def cone_hull_expl[of "{(1 :: real)} <*> S"] by auto
-  hence "rel_interior (f c)= (op *\<^sub>R c ` rel_interior S)"
-     using rel_interior_convex_scaleR[of S c] assms by auto
-}
-hence ?thesis using * ** by auto
-} ultimately show ?thesis by blast
-qed
-
+  fixes S :: "'m::euclidean_space set"
+  assumes "convex S"
+  shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} <*> S)) \<longleftrightarrow>
+    c > 0 \<and> x \<in> ((op *\<^sub>R c) ` (rel_interior S))"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    by (simp add: rel_interior_empty cone_hull_empty)
+next
+  case False
+  then obtain s where "s \<in> S" by auto
+  have conv: "convex ({(1 :: real)} <*> 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)) =
+    (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 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 "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
+  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
+    then have "rel_interior (f c) = op *\<^sub>R c ` rel_interior S"
+      using rel_interior_convex_scaleR[of S c] assms by auto
+  }
+  then show ?thesis using * ** by auto
+qed
 
 lemma rel_interior_convex_cone:
-fixes S :: "('m::euclidean_space) set"
-assumes "convex S"
-shows "rel_interior (cone hull ({(1 :: real)} <*> S)) =
-       {(c,c *\<^sub>R x) |c x. c>0 & x : (rel_interior S)}"
-(is "?lhs=?rhs")
-proof-
-{ fix z assume "z:?lhs"
-  have *: "z=(fst z,snd z)" by auto
-  have "z:?rhs" using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms `z:?lhs` apply auto
-     apply (rule_tac x="fst z" in exI) apply (rule_tac x="x" in exI) using * by auto
-}
-moreover
-{ fix z assume "z:?rhs" hence "z:?lhs"
-  using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms by auto
-}
-ultimately show ?thesis by blast
+  fixes S :: "'m::euclidean_space set"
+  assumes "convex S"
+  shows "rel_interior (cone hull ({1 :: real} <*> S)) =
+    {(c, c *\<^sub>R x) | c x. c > 0 \<and> x \<in> rel_interior S}"
+  (is "?lhs = ?rhs")
+proof -
+  {
+    fix z
+    assume "z \<in> ?lhs"
+    have *: "z = (fst z, snd z)"
+      by auto
+    have "z \<in> ?rhs"
+      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms `z \<in> ?lhs`
+      apply auto
+      apply (rule_tac x = "fst z" in exI)
+      apply (rule_tac x = x in exI)
+      using *
+      apply auto
+      done
+  }
+  moreover
+  {
+    fix z
+    assume "z \<in> ?rhs"
+    then have "z \<in> ?lhs"
+      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms
+      by auto
+  }
+  ultimately show ?thesis by blast
 qed
 
 lemma convex_hull_finite_union:
-assumes "finite I"
-assumes "!i:I. (convex (S i) & (S i) ~= {})"
-shows "convex hull (Union (S ` I)) =
-       {setsum (%i. c i *\<^sub>R s i) I |c s. (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. s i : S i)}"
+  assumes "finite I"
+  assumes "\<forall>i\<in>I. convex (S i) \<and> (S i) \<noteq> {}"
+  shows "convex hull (\<Union>(S ` I)) =
+    {setsum (\<lambda>i. c i *\<^sub>R s i) I | c s. (\<forall>i\<in>I. c i \<ge> 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. s i \<in> S i)}"
   (is "?lhs = ?rhs")
-proof-
-{ fix x assume "x : ?rhs"
-  from this obtain c s
-    where *: "setsum (%i. c i *\<^sub>R s i) I=x" "(setsum c I = 1)"
-     "(!i:I. c i >= 0) & (!i:I. s i : S i)" by auto
-  hence "!i:I. s i : convex hull (Union (S ` I))" using hull_subset[of "Union (S ` I)" convex] by auto
-  hence "x : ?lhs" unfolding *(1)[symmetric]
-     apply (subst convex_setsum[of I "convex hull Union (S ` I)" c s])
-     using * assms convex_convex_hull by auto
-} hence "?lhs >= ?rhs" by auto
-
-{ fix i assume "i:I"
-    from this assms have "EX p. p : S i" by auto
-}
-from this obtain p where p_def: "!i:I. p i : S i" by metis
-
-{ fix i assume "i:I"
-  { fix x assume "x : S i"
-    def c == "(%j. if (j=i) then (1::real) else 0)"
-    hence *: "setsum c I = 1" using `finite I` `i:I` setsum_delta[of I i "(%(j::'a). (1::real))"] by auto
-    def s == "(%j. if (j=i) then x else p j)"
-    hence "!j. c j *\<^sub>R s j = (if (j=i) then x else 0)" using c_def by (auto simp add: algebra_simps)
-    hence "x = setsum (%i. c i *\<^sub>R s i) I"
-       using s_def c_def `finite I` `i:I` setsum_delta[of I i "(%(j::'a). x)"] by auto
-    hence "x : ?rhs" apply auto
-      apply (rule_tac x="c" in exI)
-      apply (rule_tac x="s" in exI) using * c_def s_def p_def `x : S i` by auto
-  } hence "?rhs >= S i" by auto
-} hence *: "?rhs >= Union (S ` I)" by auto
-
-{ fix u v assume uv: "(u :: real)>=0 & v>=0 & u+v=1"
-  fix x y assume xy: "(x : ?rhs) & (y : ?rhs)"
-  from xy obtain c s where xc: "x=setsum (%i. c i *\<^sub>R s i) I &
-     (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. s i : S i)" by auto
-  from xy obtain d t where yc: "y=setsum (%i. d i *\<^sub>R t i) I &
-     (!i:I. d i >= 0) & (setsum d I = 1) & (!i:I. t i : S i)" by auto
-  def e == "(%i. u * (c i)+v * (d i))"
-  have ge0: "!i:I. e i >= 0"  using e_def xc yc uv by (simp add: mult_nonneg_nonneg)
-  have "setsum (%i. u * c i) I = u * setsum c I" by (simp add: setsum_right_distrib)
-  moreover have "setsum (%i. v * d i) I = v * setsum d I" by (simp add: setsum_right_distrib)
-  ultimately have sum1: "setsum e I = 1" using e_def xc yc uv by (simp add: setsum_addf)
-  def q == "(%i. if (e i = 0) then (p i)
-                 else (u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))"
-  { fix i assume "i:I"
-    { assume "e i = 0" hence "q i : S i" using `i:I` p_def q_def by auto }
-    moreover
-    { assume "e i ~= 0"
-      hence "q i : S i" using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
-         mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
-         assms q_def e_def `i:I` `e i ~= 0` xc yc uv by auto
-    } ultimately have "q i : S i" by auto
-  } hence qs: "!i:I. q i : S i" by auto
-  { fix i assume "i:I"
-    { assume "e i = 0"
-      have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg)
-      moreover from ge have "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp
-      ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto
-      hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
-         using `e i = 0` by auto
+proof -
+  have "?lhs \<supseteq> ?rhs"
+  proof
+    fix x
+    assume "x : ?rhs"
+    then obtain c s where *: "setsum (\<lambda>i. c i *\<^sub>R s i) I = x" "setsum c I = 1"
+      "(\<forall>i\<in>I. c i \<ge> 0) \<and> (\<forall>i\<in>I. s i \<in> S i)" by auto
+    then have "\<forall>i\<in>I. s i \<in> convex hull (\<Union>(S ` I))"
+      using hull_subset[of "\<Union>(S ` I)" convex] by auto
+    then show "x \<in> ?lhs"
+      unfolding *(1)[symmetric]
+      apply (subst convex_setsum[of I "convex hull \<Union>(S ` I)" c s])
+      using * assms convex_convex_hull
+      apply auto
+      done
+  qed
+
+  {
+    fix i
+    assume "i \<in> I"
+    with assms have "\<exists>p. p \<in> S i" by auto
+  }
+  then obtain p where p: "\<forall>i\<in>I. p i \<in> S i" by metis
+
+  {
+    fix i
+    assume "i \<in> I"
+    {
+      fix x
+      assume "x \<in> S i"
+      def c \<equiv> "\<lambda>j. if j = i then 1::real else 0"
+      then have *: "setsum c I = 1"
+        using `finite I` `i \<in> I` setsum_delta[of I i "\<lambda>j::'a. 1::real"]
+        by auto
+      def s \<equiv> "\<lambda>j. if j = i then x else p j"
+      then have "\<forall>j. c j *\<^sub>R s j = (if j = i then x else 0)"
+        using c_def by (auto simp add: algebra_simps)
+      then have "x = setsum (\<lambda>i. c i *\<^sub>R s i) I"
+        using s_def c_def `finite I` `i \<in> I` setsum_delta[of I i "\<lambda>j::'a. x"]
+        by auto
+      then have "x \<in> ?rhs"
+        apply auto
+        apply (rule_tac x = c in exI)
+        apply (rule_tac x = s in exI)
+        using * c_def s_def p `x \<in> S i`
+        apply auto
+        done
     }
-    moreover
-    { assume "e i ~= 0"
-      hence "(u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i) = q i"
-         using q_def by auto
-      hence "e i *\<^sub>R ((u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))
-             = (e i) *\<^sub>R (q i)" by auto
-      hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
-         using `e i ~= 0` by (simp add: algebra_simps)
-    } ultimately have
-      "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by blast
-  } hence *: "!i:I.
-    (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" by auto
-  have "u *\<^sub>R x + v *\<^sub>R y =
-       setsum (%i. (u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i)) I"
-          using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum_addf)
-  also have "...=setsum (%i. (e i) *\<^sub>R (q i)) I" using * by auto
-  finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto
-  hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto
-} hence "convex ?rhs" unfolding convex_def by auto
-from this show ?thesis using `?lhs >= ?rhs` *
-   hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast
+    then have "?rhs \<supseteq> S i" by auto
+  }
+  then have *: "?rhs \<supseteq> \<Union>(S ` I)" by auto
+
+  {
+    fix u v :: real
+    assume uv: "u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1"
+    fix x y
+    assume xy: "x \<in> ?rhs \<and> y \<in> ?rhs"
+    from xy obtain c s where
+      xc: "x = setsum (\<lambda>i. c i *\<^sub>R s i) I \<and> (\<forall>i\<in>I. c i \<ge> 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. s i \<in> S i)"
+      by auto
+    from xy obtain d t where
+      yc: "y = setsum (\<lambda>i. d i *\<^sub>R t i) I \<and> (\<forall>i\<in>I. d i \<ge> 0) \<and> setsum d I = 1 \<and> (\<forall>i\<in>I. t i \<in> S i)"
+      by auto
+    def e \<equiv> "\<lambda>i. u * c i + v * d i"
+    have ge0: "\<forall>i\<in>I. e i \<ge> 0"
+      using e_def xc yc uv by (simp add: mult_nonneg_nonneg)
+    have "setsum (\<lambda>i. u * c i) I = u * setsum c I"
+      by (simp add: setsum_right_distrib)
+    moreover have "setsum (\<lambda>i. v * d i) I = v * setsum d I"
+      by (simp add: setsum_right_distrib)
+    ultimately have sum1: "setsum e I = 1"
+      using e_def xc yc uv by (simp add: setsum_addf)
+    def q \<equiv> "\<lambda>i. if e i = 0 then p i else (u * c i / e i) *\<^sub>R s i + (v * d i / e i) *\<^sub>R t i"
+    {
+      fix i
+      assume i: "i \<in> I"
+      have "q i \<in> S i"
+      proof (cases "e i = 0")
+        case True
+        then show ?thesis using i p q_def by auto
+      next
+        case False
+        then show ?thesis
+          using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
+            mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
+            assms q_def e_def i False xc yc uv
+          by auto
+      qed
+    }
+    then have qs: "\<forall>i\<in>I. q i \<in> S i" by auto
+    {
+      fix i
+      assume i: "i \<in> I"
+      have "(u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i = e i *\<^sub>R q i"
+      proof (cases "e i = 0")
+        case True
+        have ge: "u * (c i) \<ge> 0 \<and> v * d i \<ge> 0"
+          using xc yc uv i by (simp add: mult_nonneg_nonneg)
+        moreover from ge have "u * c i \<le> 0 \<and> v * d i \<le> 0"
+          using True e_def i by simp
+        ultimately have "u * c i = 0 \<and> v * d i = 0" by auto
+        with True show ?thesis by auto
+      next
+        case False
+        then have "(u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i) = q i"
+          using q_def by auto
+        then have "e i *\<^sub>R ((u * (c i)/(e i))*\<^sub>R (s i)+(v * (d i)/(e i))*\<^sub>R (t i))
+               = (e i) *\<^sub>R (q i)" by auto
+        with False show ?thesis by (simp add: algebra_simps)
+      qed
+    }
+    then have *: "\<forall>i\<in>I. (u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i = e i *\<^sub>R q i"
+      by auto
+    have "u *\<^sub>R x + v *\<^sub>R y = setsum (\<lambda>i. (u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i) I"
+      using xc yc by (simp add: algebra_simps scaleR_right.setsum setsum_addf)
+    also have "\<dots> = setsum (\<lambda>i. e i *\<^sub>R q i) I"
+      using * by auto
+    finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (\<lambda>i. (e i) *\<^sub>R (q i)) I"
+      by auto
+    then have "u *\<^sub>R x + v *\<^sub>R y \<in> ?rhs"
+      using ge0 sum1 qs by auto
+  }
+  then have "convex ?rhs" unfolding convex_def by auto
+  then show ?thesis
+    using `?lhs \<supseteq> ?rhs` * hull_minimal[of "\<Union>(S ` I)" ?rhs convex]
+    by blast
 qed
 
 lemma convex_hull_union_two:
-fixes S T :: "('m::euclidean_space) set"
-assumes "convex S" "S ~= {}" "convex T" "T ~= {}"
-shows "convex hull (S Un T) = {u *\<^sub>R s + v *\<^sub>R t |u v s t. u>=0 & v>=0 & u+v=1 & s:S & t:T}"
+  fixes S T :: "'m::euclidean_space set"
+  assumes "convex S"
+    and "S \<noteq> {}"
+    and "convex T"
+    and "T \<noteq> {}"
+  shows "convex hull (S \<union> T) =
+    {u *\<^sub>R s + v *\<^sub>R t | u v s t. u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1 \<and> s \<in> S \<and> t \<in> T}"
   (is "?lhs = ?rhs")
-proof-
-def I == "{(1::nat),2}"
-def s == "(%i. (if i=(1::nat) then S else T))"
-have "Union (s ` I) = S Un T" using s_def I_def by auto
-hence "convex hull (Union (s ` I)) = convex hull (S Un T)" by auto
-moreover have "convex hull Union (s ` I) =
-    {SUM i:I. c i *\<^sub>R sa i |c sa. (ALL i:I. 0 <= c i) & setsum c I = 1 & (ALL i:I. sa i : s i)}"
-    apply (subst convex_hull_finite_union[of I s]) using assms s_def I_def by auto
-moreover have
-  "{SUM i:I. c i *\<^sub>R sa i |c sa. (ALL i:I. 0 <= c i) & setsum c I = 1 & (ALL i:I. sa i : s i)} <=
-  ?rhs"
-  using s_def I_def by auto
-ultimately have "?lhs<=?rhs" by auto
-{ fix x assume "x : ?rhs"
-  from this obtain u v s t
-    where *: "x=u *\<^sub>R s + v *\<^sub>R t & u>=0 & v>=0 & u+v=1 & s:S & t:T" by auto
-  hence "x : convex hull {s,t}" using convex_hull_2[of s t] by auto
-  hence "x : convex hull (S Un T)" using * hull_mono[of "{s, t}" "S Un T"] by auto
-} hence "?lhs >= ?rhs" by blast
-from this show ?thesis using `?lhs<=?rhs` by auto
-qed
+proof
+  def I \<equiv> "{1::nat, 2}"
+  def s \<equiv> "\<lambda>i. if i = (1::nat) then S else T"
+  have "\<Union>(s ` I) = S \<union> T"
+    using s_def I_def by auto
+  then have "convex hull (\<Union>(s ` I)) = convex hull (S \<union> T)"
+    by auto
+  moreover have "convex hull \<Union>(s ` I) =
+    {\<Sum> i\<in>I. c i *\<^sub>R sa i | c sa. (\<forall>i\<in>I. 0 \<le> c i) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. sa i \<in> s i)}"
+      apply (subst convex_hull_finite_union[of I s])
+      using assms s_def I_def
+      apply auto
+      done
+  moreover have
+    "{\<Sum>i\<in>I. c i *\<^sub>R sa i | c sa. (\<forall>i\<in>I. 0 \<le> c i) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. sa i \<in> s i)} \<le> ?rhs"
+    using s_def I_def by auto
+  ultimately show "?lhs \<subseteq> ?rhs" by auto
+  {
+    fix x
+    assume "x \<in> ?rhs"
+    then obtain u v s t where *: "x = u *\<^sub>R s + v *\<^sub>R t \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1 \<and> s \<in> S \<and> t \<in> T"
+      by auto
+    then have "x \<in> convex hull {s, t}"
+      using convex_hull_2[of s t] by auto
+    then have "x \<in> convex hull (S \<union> T)"
+      using * hull_mono[of "{s, t}" "S \<union> T"] by auto
+  }
+  then show "?lhs \<supseteq> ?rhs" by blast
+qed
+
 
 subsection {* Convexity on direct sums *}
 
 lemma closure_sum:
-  fixes S T :: "('n::euclidean_space) set"
+  fixes S T :: "'n::euclidean_space set"
   shows "closure S + closure T \<subseteq> closure (S + T)"
-proof-
-  have "(closure S) + (closure T) = (\<lambda>(x,y). x + y) ` (closure S \<times> closure T)"
+proof -
+  have "closure S + closure T = (\<lambda>(x,y). x + y) ` (closure S \<times> closure T)"
     by (simp add: set_plus_image)
-  also have "... = (\<lambda>(x,y). x + y) ` closure (S \<times> T)"
+  also have "\<dots> = (\<lambda>(x,y). x + y) ` closure (S \<times> T)"
     using closure_Times by auto
-  also have "... \<subseteq> closure (S + T)"
+  also have "\<dots> \<subseteq> closure (S + T)"
     using fst_snd_linear closure_linear_image[of "(\<lambda>(x,y). x + y)" "S \<times> T"]
     by (auto simp: set_plus_image)
   finally show ?thesis
@@ -8482,216 +8597,345 @@
 qed
 
 lemma convex_oplus:
-fixes S T :: "('n::euclidean_space) set"
-assumes "convex S" "convex T"
-shows "convex (S + T)"
-proof-
-have "{x + y |x y. x : S & y : T} = {c. EX a:S. EX b:T. c = a + b}" by auto
-thus ?thesis unfolding set_plus_def using convex_sums[of S T] assms by auto
+  fixes S T :: "'n::euclidean_space set"
+  assumes "convex S"
+    and "convex T"
+  shows "convex (S + T)"
+proof -
+  have "{x + y |x y. x \<in> S \<and> y \<in> T} = {c. \<exists>a\<in>S. \<exists>b\<in>T. c = a + b}"
+    by auto
+  then show ?thesis
+    unfolding set_plus_def
+    using convex_sums[of S T] assms
+    by auto
 qed
 
 lemma convex_hull_sum:
-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) =
-      (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
-   by (simp add: set_plus_image)
-also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_Times by auto
-also have "...= convex hull (S + T)" using fst_snd_linear linear_conv_bounded_linear
-   convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
-finally show ?thesis by auto
+  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))"
+    by (simp add: set_plus_image)
+  also have "\<dots> = (\<lambda>(x,y). x + y) ` (convex hull (S <*> 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"]
+    by (auto simp add: set_plus_image)
+  finally show ?thesis ..
 qed
 
 lemma rel_interior_sum:
-fixes S T :: "('n::euclidean_space) set"
-assumes "convex S" "convex T"
-shows "rel_interior (S + T) = (rel_interior S) + (rel_interior T)"
-proof-
-have "(rel_interior S) + (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
-   by (simp add: set_plus_image)
-also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
-also have "...= rel_interior (S + T)" using fst_snd_linear convex_Times assms
-   rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
-finally show ?thesis by auto
+  fixes S T :: "'n::euclidean_space set"
+  assumes "convex S"
+    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)"
+    by (simp add: set_plus_image)
+  also have "\<dots> = (\<lambda>(x,y). x + y) ` rel_interior (S <*> 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"]
+    by (auto simp add: set_plus_image)
+  finally show ?thesis ..
 qed
 
 lemma convex_sum_gen:
   fixes S :: "'a \<Rightarrow> 'n::euclidean_space set"
   assumes "\<And>i. i \<in> I \<Longrightarrow> (convex (S i))"
   shows "convex (setsum S I)"
-proof cases
-  assume "finite I" from this assms show ?thesis
+proof (cases "finite I")
+  case True
+  from this and assms show ?thesis
     by induct (auto simp: convex_oplus)
-qed auto
+next
+  case False
+  then show ?thesis by auto
+qed
 
 lemma convex_hull_sum_gen:
-fixes S :: "'a => ('n::euclidean_space) set"
-shows "convex hull (setsum S I) = setsum (%i. (convex hull (S i))) I"
-apply (subst setsum_set_linear) using convex_hull_sum convex_hull_singleton by auto
-
+  fixes S :: "'a \<Rightarrow> 'n::euclidean_space set"
+  shows "convex hull (setsum S I) = setsum (\<lambda>i. convex hull (S i)) I"
+  apply (subst setsum_set_linear)
+  using convex_hull_sum convex_hull_singleton
+  apply auto
+  done
 
 lemma rel_interior_sum_gen:
-fixes S :: "'a => ('n::euclidean_space) set"
-assumes "!i:I. (convex (S i))"
-shows "rel_interior (setsum S I) = setsum (%i. (rel_interior (S i))) I"
-apply (subst setsum_set_cond_linear[of convex])
-  using rel_interior_sum rel_interior_sing[of "0"] assms by (auto simp add: convex_oplus)
+  fixes S :: "'a \<Rightarrow> 'n::euclidean_space set"
+  assumes "\<forall>i\<in>I. convex (S i)"
+  shows "rel_interior (setsum S I) = setsum (\<lambda>i. rel_interior (S i)) I"
+  apply (subst setsum_set_cond_linear[of convex])
+  using rel_interior_sum rel_interior_sing[of "0"] assms
+  apply (auto simp add: convex_oplus)
+  done
 
 lemma convex_rel_open_direct_sum:
-fixes S T :: "('n::euclidean_space) set"
-assumes "convex S" "rel_open S" "convex T" "rel_open T"
-shows "convex (S <*> T) & rel_open (S <*> T)"
-by (metis assms convex_Times rel_interior_direct_sum rel_open_def)
+  fixes S T :: "'n::euclidean_space set"
+  assumes "convex S"
+    and "rel_open S"
+    and "convex T"
+    and "rel_open T"
+  shows "convex (S <*> T) \<and> rel_open (S <*> T)"
+  by (metis assms convex_Times rel_interior_direct_sum rel_open_def)
 
 lemma convex_rel_open_sum:
-fixes S T :: "('n::euclidean_space) set"
-assumes "convex S" "rel_open S" "convex T" "rel_open T"
-shows "convex (S + T) & rel_open (S + T)"
-by (metis assms convex_oplus rel_interior_sum rel_open_def)
+  fixes S T :: "'n::euclidean_space set"
+  assumes "convex S"
+    and "rel_open S"
+    and "convex T"
+    and "rel_open T"
+  shows "convex (S + T) \<and> rel_open (S + T)"
+  by (metis assms convex_oplus rel_interior_sum rel_open_def)
 
 lemma convex_hull_finite_union_cones:
-assumes "finite I" "I ~= {}"
-assumes "!i:I. (convex (S i) & cone (S i) & (S i) ~= {})"
-shows "convex hull (Union (S ` I)) = setsum S I"
+  assumes "finite I"
+    and "I \<noteq> {}"
+  assumes "\<forall>i\<in>I. convex (S i) \<and> cone (S i) \<and> S i \<noteq> {}"
+  shows "convex hull (\<Union>(S ` I)) = setsum S I"
   (is "?lhs = ?rhs")
-proof-
-{ fix x assume "x : ?lhs"
-  from this obtain c xs where x_def: "x=setsum (%i. c i *\<^sub>R xs i) I &
-     (!i:I. c i >= 0) & (setsum c I = 1) & (!i:I. xs i : S i)"
-     using convex_hull_finite_union[of I S] assms by auto
-  def s == "(%i. c i *\<^sub>R xs i)"
-  { fix i assume "i:I"
-    hence "s i : S i" using s_def x_def assms mem_cone[of "S i" "xs i" "c i"] by auto
-  } hence "!i:I. s i : S i" by auto
-  moreover have "x = setsum s I" using x_def s_def by auto
-  ultimately have "x : ?rhs" using set_setsum_alt[of I S] assms by auto
-}
-moreover
-{ fix x assume "x : ?rhs"
-  from this obtain s where x_def: "x=setsum s I & (!i:I. s i : S i)"
-     using set_setsum_alt[of I S] assms by auto
-  def xs == "(%i. of_nat(card I) *\<^sub>R s i)"
-  hence "x=setsum (%i. ((1 :: real)/of_nat(card I)) *\<^sub>R xs i) I" using x_def assms by auto
-  moreover have "!i:I. xs i : S i" using x_def xs_def assms by (simp add: cone_def)
-  moreover have "(!i:I. (1 :: real)/of_nat(card I) >= 0)" by auto
-  moreover have "setsum (%i. (1 :: real)/of_nat(card I)) I = 1" using assms by auto
-  ultimately have "x : ?lhs" apply (subst convex_hull_finite_union[of I S])
-    using assms apply blast
-    using assms apply blast
-    apply rule apply (rule_tac x="(%i. (1 :: real)/of_nat(card I))" in exI) by auto
-} ultimately show ?thesis by auto
+proof -
+  {
+    fix x
+    assume "x \<in> ?lhs"
+    then obtain c xs where
+      x: "x = setsum (\<lambda>i. c i *\<^sub>R xs i) I \<and> (\<forall>i\<in>I. c i \<ge> 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. xs i \<in> S i)"
+      using convex_hull_finite_union[of I S] assms by auto
+    def s \<equiv> "\<lambda>i. c i *\<^sub>R xs i"
+    {
+      fix i
+      assume "i \<in> I"
+      then have "s i \<in> S i"
+        using s_def x assms mem_cone[of "S i" "xs i" "c i"] by auto
+    }
+    then have "\<forall>i\<in>I. s i \<in> S i" by auto
+    moreover have "x = setsum s I" using x s_def by auto
+    ultimately have "x \<in> ?rhs"
+      using set_setsum_alt[of I S] assms by auto
+  }
+  moreover
+  {
+    fix x
+    assume "x \<in> ?rhs"
+    then obtain s where x: "x = setsum s I \<and> (\<forall>i\<in>I. s i \<in> S i)"
+      using set_setsum_alt[of I S] assms by auto
+    def xs \<equiv> "\<lambda>i. of_nat(card I) *\<^sub>R s i"
+    then have "x = setsum (\<lambda>i. ((1 :: real) / of_nat(card I)) *\<^sub>R xs i) I"
+      using x assms by auto
+    moreover have "\<forall>i\<in>I. xs i \<in> S i"
+      using x xs_def assms by (simp add: cone_def)
+    moreover have "\<forall>i\<in>I. (1 :: real) / of_nat (card I) \<ge> 0"
+      by auto
+    moreover have "setsum (\<lambda>i. (1 :: real) / of_nat (card I)) I = 1"
+      using assms by auto
+    ultimately have "x \<in> ?lhs"
+      apply (subst convex_hull_finite_union[of I S])
+      using assms
+      apply blast
+      using assms
+      apply blast
+      apply rule
+      apply (rule_tac x = "(\<lambda>i. (1 :: real) / of_nat (card I))" in exI)
+      apply auto
+      done
+  }
+  ultimately show ?thesis by auto
 qed
 
 lemma convex_hull_union_cones_two:
-fixes S T :: "('m::euclidean_space) set"
-assumes "convex S" "cone S" "S ~= {}"
-assumes "convex T" "cone T" "T ~= {}"
-shows "convex hull (S Un T) = S + T"
-proof-
-def I == "{(1::nat),2}"
-def A == "(%i. (if i=(1::nat) then S else T))"
-have "Union (A ` I) = S Un T" using A_def I_def by auto
-hence "convex hull (Union (A ` I)) = convex hull (S Un T)" by auto
-moreover have "convex hull Union (A ` I) = setsum A I"
-    apply (subst convex_hull_finite_union_cones[of I A]) using assms A_def I_def by auto
-moreover have
-  "setsum A I = S + T" using A_def I_def
-     unfolding set_plus_def apply auto unfolding set_plus_def by auto
-ultimately show ?thesis by auto
+  fixes S T :: "'m::euclidean_space set"
+  assumes "convex S"
+    and "cone S"
+    and "S \<noteq> {}"
+  assumes "convex T"
+    and "cone T"
+    and "T \<noteq> {}"
+  shows "convex hull (S \<union> T) = S + T"
+proof -
+  def I \<equiv> "{1::nat, 2}"
+  def A \<equiv> "(\<lambda>i. if i = (1::nat) then S else T)"
+  have "\<Union>(A ` I) = S \<union> T"
+    using A_def I_def by auto
+  then have "convex hull (\<Union>(A ` I)) = convex hull (S \<union> T)"
+    by auto
+  moreover have "convex hull \<Union>(A ` I) = setsum A I"
+    apply (subst convex_hull_finite_union_cones[of I A])
+    using assms A_def I_def
+    apply auto
+    done
+  moreover have "setsum A I = S + T"
+    using A_def I_def
+    unfolding set_plus_def
+    apply auto
+    unfolding set_plus_def
+    apply auto
+    done
+  ultimately show ?thesis by auto
 qed
 
 lemma rel_interior_convex_hull_union:
-fixes S :: "'a => ('n::euclidean_space) set"
-assumes "finite I"
-assumes "!i:I. convex (S i) & (S i) ~= {}"
-shows "rel_interior (convex hull (Union (S ` I))) =  {setsum (%i. c i *\<^sub>R s i) I
-       |c s. (!i:I. c i > 0) & (setsum c I = 1) & (!i:I. s i : rel_interior(S i))}"
-(is "?lhs=?rhs")
-proof-
-{ assume "I={}" hence ?thesis using convex_hull_empty rel_interior_empty by auto }
-moreover
-{ assume "I ~= {}"
-  def C0 == "convex hull (Union (S ` I))"
-  have "!i:I. C0 >= S i" unfolding C0_def using hull_subset[of "Union (S ` I)"] by auto
-  def K0 == "cone hull ({(1 :: real)} <*> C0)"
-  def K == "(%i. cone hull ({(1 :: real)} <*> (S i)))"
-  have "!i:I. K i ~= {}" unfolding K_def using assms by (simp add: cone_hull_empty_iff[symmetric])
-  { fix i assume "i:I"
-    hence "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_Times)
-    using assms by auto
+  fixes S :: "'a \<Rightarrow> 'n::euclidean_space set"
+  assumes "finite I"
+    and "\<forall>i\<in>I. convex (S i) \<and> S i \<noteq> {}"
+  shows "rel_interior (convex hull (\<Union>(S ` I))) =
+    {setsum (\<lambda>i. c i *\<^sub>R s i) I | c s. (\<forall>i\<in>I. c i > 0) \<and> setsum c I = 1 \<and>
+      (\<forall>i\<in>I. s i \<in> rel_interior(S i))}"
+  (is "?lhs = ?rhs")
+proof (cases "I = {}")
+  case True
+  then show ?thesis
+    using convex_hull_empty rel_interior_empty by auto
+next
+  case False
+  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)"
+  have "\<forall>i\<in>I. K i \<noteq> {}"
+    unfolding K_def using assms
+    by (simp add: cone_hull_empty_iff[symmetric])
+  {
+    fix i
+    assume "i \<in> I"
+    then have "convex (K i)"
+      unfolding K_def
+      apply (subst convex_cone_hull)
+      apply (subst convex_Times)
+      using assms
+      apply auto
+      done
   }
-  hence convK: "!i:I. convex (K i)" by auto
-  { fix i assume "i:I"
-    hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto
+  then have convK: "\<forall>i\<in>I. convex (K i)"
+    by auto
+  {
+    fix i
+    assume "i \<in> I"
+    then have "K0 \<supseteq> K i"
+      unfolding K0_def K_def
+      apply (subst hull_mono)
+      using `\<forall>i\<in>I. C0 \<ge> S i`
+      apply auto
+      done
   }
-  hence "K0 >= Union (K ` I)" by auto
-  moreover have "convex K0" unfolding K0_def
-     apply (subst convex_cone_hull) apply (subst convex_Times)
-     unfolding C0_def using convex_convex_hull by auto
-  ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
-  have "!i:I. K i >= {(1 :: real)} <*> (S i)" using K_def by (simp add: hull_subset)
-  hence "Union (K ` I) >= {(1 :: real)} <*> Union (S ` I)" by auto
-  hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
-  hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
-     using convex_hull_Times[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
-  moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull)
-     using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
-  ultimately have "convex hull (Union (K ` I)) >= K0"
-     unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast
-  hence "K0 = convex hull (Union (K ` I))" using geq by auto
-  also have "...=setsum K I"
-     apply (subst convex_hull_finite_union_cones[of I K])
-     using assms apply blast
-     using `I ~= {}` apply blast
-     unfolding K_def apply rule
-     apply (subst convex_cone_hull) apply (subst convex_Times)
-     using assms cone_cone_hull `!i:I. K i ~= {}` K_def by auto
+  then have "K0 \<supseteq> \<Union>(K ` I)" by auto
+  moreover have "convex K0"
+    unfolding K0_def
+    apply (subst convex_cone_hull)
+    apply (subst convex_Times)
+    unfolding C0_def
+    using convex_convex_hull
+    apply auto
+    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"
+    using K_def by (simp add: hull_subset)
+  then have "\<Union>(K ` I) \<supseteq> {1 :: real} <*> \<Union>(S ` I)"
+    by auto
+  then have "convex hull \<Union>(K ` I) \<supseteq> convex hull ({1 :: real} <*> \<Union>(S ` I))"
+    by (simp add: hull_mono)
+  then have "convex hull \<Union>(K ` I) \<supseteq> {1 :: real} <*> C0"
+    unfolding C0_def
+    using convex_hull_Times[of "{(1 :: real)}" "\<Union>(S ` I)"] convex_hull_singleton
+    by auto
+  moreover have "cone (convex hull (\<Union>(K ` I)))"
+    apply (subst cone_convex_hull)
+    using cone_Union[of "K ` I"]
+    apply auto
+    unfolding K_def
+    using cone_cone_hull
+    apply auto
+    done
+  ultimately have "convex hull (\<Union>(K ` I)) \<supseteq> K0"
+    unfolding K0_def
+    using hull_minimal[of _ "convex hull (\<Union> (K ` I))" "cone"]
+    by blast
+  then have "K0 = convex hull (\<Union>(K ` I))"
+    using geq by auto
+  also have "\<dots> = setsum K I"
+    apply (subst convex_hull_finite_union_cones[of I K])
+    using assms
+    apply blast
+    using False
+    apply blast
+    unfolding K_def
+    apply rule
+    apply (subst convex_cone_hull)
+    apply (subst convex_Times)
+    using assms cone_cone_hull `\<forall>i\<in>I. K i \<noteq> {}` K_def
+    apply auto
+    done
   finally have "K0 = setsum K I" by auto
-  hence *: "rel_interior K0 = setsum (%i. (rel_interior (K i))) I"
-     using rel_interior_sum_gen[of I K] convK by auto
-  { fix x assume "x : ?lhs"
-    hence "((1::real),x) : rel_interior K0" using K0_def C0_def
-       rel_interior_convex_cone_aux[of C0 "(1::real)" x] convex_convex_hull by auto
-    from this obtain k where k_def: "((1::real),x) = setsum k I & (!i:I. k i : rel_interior (K i))"
-      using `finite I` * set_setsum_alt[of I "(%i. rel_interior (K i))"] by auto
-    { fix i assume "i:I"
-      hence "(convex (S i)) & k i : rel_interior (cone hull {1} <*> S i)" using k_def K_def assms by auto
-      hence "EX ci si. k i = (ci, ci *\<^sub>R si) & 0 < ci & si : rel_interior (S i)"
-         using rel_interior_convex_cone[of "S i"] by auto
+  then have *: "rel_interior K0 = setsum (\<lambda>i. (rel_interior (K i))) I"
+    using rel_interior_sum_gen[of I K] convK by auto
+  {
+    fix x
+    assume "x \<in> ?lhs"
+    then have "(1::real, x) \<in> rel_interior K0"
+      using K0_def C0_def rel_interior_convex_cone_aux[of C0 "1::real" x] convex_convex_hull
+      by auto
+    then obtain k where k: "(1::real, x) = setsum k I \<and> (\<forall>i\<in>I. k i \<in> rel_interior (K i))"
+      using `finite I` * set_setsum_alt[of I "\<lambda>i. rel_interior (K i)"] by auto
+    {
+      fix i
+      assume "i \<in> I"
+      then have "convex (S i) \<and> k i \<in> rel_interior (cone hull {1} <*> 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
     }
-    from this obtain c s where cs_def: "!i:I. (k i = (c i, c i *\<^sub>R s i) & 0 < c i
-          & s i : rel_interior (S i))" by metis
-    hence "x = (SUM i:I. c i *\<^sub>R s i) & setsum c I = 1" using k_def by (simp add: setsum_prod)
-    hence "x : ?rhs" using k_def apply auto
-       apply (rule_tac x="c" in exI) apply (rule_tac x="s" in exI) using cs_def by auto
+    then obtain c s where
+      cs: "\<forall>i\<in>I. k i = (c i, c i *\<^sub>R s i) \<and> 0 < c i \<and> s i \<in> rel_interior (S i)"
+      by metis
+    then have "x = (\<Sum>i\<in>I. c i *\<^sub>R s i) \<and> setsum c I = 1"
+      using k by (simp add: setsum_prod)
+    then have "x \<in> ?rhs"
+      using k
+      apply auto
+      apply (rule_tac x = c in exI)
+      apply (rule_tac x = s in exI)
+      using cs
+      apply auto
+      done
   }
   moreover
-  { fix x assume "x : ?rhs"
-    from this obtain c s where cs_def: "x=setsum (%i. c i *\<^sub>R s i) I &
-       (!i:I. c i > 0) & (setsum c I = 1) & (!i:I. s i : rel_interior(S i))" by auto
-    def k == "(%i. (c i, c i *\<^sub>R s i))"
-    { fix i assume "i:I"
-      hence "k i : rel_interior (K i)"
-         using k_def K_def assms cs_def rel_interior_convex_cone[of "S i"] by auto
+  {
+    fix x
+    assume "x \<in> ?rhs"
+    then obtain c s where cs: "x = setsum (\<lambda>i. c i *\<^sub>R s i) I \<and>
+        (\<forall>i\<in>I. c i > 0) \<and> setsum c I = 1 \<and> (\<forall>i\<in>I. s i \<in> rel_interior (S i))"
+      by auto
+    def k \<equiv> "\<lambda>i. (c i, c i *\<^sub>R s i)"
+    {
+      fix i assume "i:I"
+      then have "k i \<in> rel_interior (K i)"
+        using k_def K_def assms cs rel_interior_convex_cone[of "S i"]
+        by auto
     }
-    hence "((1::real),x) : rel_interior K0"
-       using K0_def * set_setsum_alt[of I "(%i. rel_interior (K i))"] assms k_def cs_def
-       apply auto apply (rule_tac x="k" in exI) by (simp add: setsum_prod)
-    hence "x : ?lhs" using K0_def C0_def
-       rel_interior_convex_cone_aux[of C0 "(1::real)" x] by (auto simp add: convex_convex_hull)
+    then have "(1::real, x) \<in> rel_interior K0"
+      using K0_def * set_setsum_alt[of I "(\<lambda>i. rel_interior (K i))"] assms k_def cs
+      apply auto
+      apply (rule_tac x = k in exI)
+      apply (simp add: setsum_prod)
+      done
+    then have "x \<in> ?lhs"
+      using K0_def C0_def rel_interior_convex_cone_aux[of C0 1 x]
+      by (auto simp add: convex_convex_hull)
   }
-  ultimately have ?thesis by blast
-} ultimately show ?thesis by blast
+  ultimately show ?thesis by blast
 qed
 
 
 lemma convex_le_Inf_differential:
   fixes f :: "real \<Rightarrow> real"
   assumes "convex_on I f"
-  assumes "x \<in> interior I" "y \<in> I"
+    and "x \<in> interior I"
+    and "y \<in> I"
   shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
-    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
+  (is "_ \<ge> _ + Inf (?F x) * (y - x)")
 proof (cases rule: linorder_cases)
   assume "x < y"
   moreover
@@ -8705,7 +8949,8 @@
   have "open (interior I)" by auto
   from openE[OF this `x \<in> interior I`] guess e .
   moreover def K \<equiv> "x - e / 2"
-  with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
+  with `0 < e` have "K \<in> ball x e" "K < x"
+    by (auto simp: dist_real_def)
   ultimately have "K \<in> I" "K < x" "x \<in> I"
     using interior_subset[of I] `x \<in> interior I` by auto
 
@@ -8714,9 +8959,11 @@
     show "(f x - f t) / (x - t) \<in> ?F x"
       using `t \<in> I` `x < t` by auto
     show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
-      using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
+      using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y`
+      by (rule convex_on_diff)
   next
-    fix y assume "y \<in> ?F x"
+    fix y
+    assume "y \<in> ?F x"
     with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
     show "(f K - f x) / (K - x) \<le> y" by auto
   qed
@@ -8737,16 +8984,21 @@
     have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
       using `y < x` by (auto simp: field_simps)
     also
-    fix z  assume "z \<in> ?F x"
+    fix z
+    assume "z \<in> ?F x"
     with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
-    have "(f y - f x) / (y - x) \<le> z" by auto
+    have "(f y - f x) / (y - x) \<le> z"
+      by auto
     finally show "(f x - f y) / (x - y) \<le> z" .
   next
     have "open (interior I)" by auto
     from openE[OF this `x \<in> interior I`] guess e . note e = this
-    then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
-    with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
-    then show "?F x \<noteq> {}" by blast
+    then have "x + e / 2 \<in> ball x e"
+      by (auto simp: dist_real_def)
+    with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I"
+      by auto
+    then show "?F x \<noteq> {}"
+      by blast
   qed
   then show ?thesis
     using `y < x` by (simp add: field_simps)