# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524859174 -3600
# Node ID e98988801fa9d06eb734e6066dd51a3a037323e6
# Parent  68def9274939821e2bae01db990a2cda4770d899
another big cleanup

diff -r 68def9274939 -r e98988801fa9 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Apr 27 12:43:05 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Apr 27 20:59:34 2018 +0100
@@ -4893,112 +4893,77 @@
 subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation\<close>
 
 lemma open_convex_hull[intro]:
-  fixes s :: "'a::real_normed_vector set"
-  assumes "open s"
-  shows "open (convex hull s)"
-  unfolding open_contains_cball convex_hull_explicit
-  unfolding mem_Collect_eq ball_simps(8)
-proof (rule, rule)
-  fix a
-  assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> sum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a"
-  then obtain t u where obt: "finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "sum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a"
-    by auto
+  fixes S :: "'a::real_normed_vector set"
+  assumes "open S"
+  shows "open (convex hull S)"
+proof (clarsimp simp: open_contains_cball convex_hull_explicit)
+  fix T and u :: "'a\<Rightarrow>real"
+  assume obt: "finite T" "T\<subseteq>S" "\<forall>x\<in>T. 0 \<le> u x" "sum u T = 1" 
 
   from assms[unfolded open_contains_cball] obtain b
-    where b: "\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s"
-    using bchoice[of s "\<lambda>x e. e > 0 \<and> cball x e \<subseteq> s"] by auto
-  have "b ` t \<noteq> {}"
+    where b: "\<And>x. x\<in>S \<Longrightarrow> 0 < b x \<and> cball x (b x) \<subseteq> S" by metis
+  have "b ` T \<noteq> {}"
     using obt by auto
-  define i where "i = b ` t"
-
-  show "\<exists>e > 0.
-    cball a e \<subseteq> {y. \<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> sum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y}"
-    apply (rule_tac x = "Min i" in exI)
-    unfolding subset_eq
-    apply rule
-    defer
-    apply rule
-    unfolding mem_Collect_eq
-  proof -
+  define i where "i = b ` T"
+  let ?\<Phi> = "\<lambda>y. \<exists>F. finite F \<and> F \<subseteq> S \<and> (\<exists>u. (\<forall>x\<in>F. 0 \<le> u x) \<and> sum u F = 1 \<and> (\<Sum>v\<in>F. u v *\<^sub>R v) = y)"
+  let ?a = "\<Sum>v\<in>T. u v *\<^sub>R v"
+  show "\<exists>e > 0. cball ?a e \<subseteq> {y. ?\<Phi> y}"
+  proof (intro exI subsetI conjI)
     show "0 < Min i"
-      unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] \<open>b ` t\<noteq>{}\<close>]
-      using b
-      apply simp
-      apply rule
-      apply (erule_tac x=x in ballE)
-      using \<open>t\<subseteq>s\<close>
-      apply auto
-      done
+      unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] \<open>b ` T\<noteq>{}\<close>]
+      using b \<open>T\<subseteq>S\<close> by auto
   next
     fix y
-    assume "y \<in> cball a (Min i)"
-    then have y: "norm (a - y) \<le> Min i"
+    assume "y \<in> cball ?a (Min i)"
+    then have y: "norm (?a - y) \<le> Min i"
       unfolding dist_norm[symmetric] by auto
-    {
-      fix x
-      assume "x \<in> t"
+    { fix x
+      assume "x \<in> T"
       then have "Min i \<le> b x"
-        unfolding i_def
-        apply (rule_tac Min_le)
-        using obt(1)
-        apply auto
-        done
-      then have "x + (y - a) \<in> cball x (b x)"
+        by (simp add: i_def obt(1))
+      then have "x + (y - ?a) \<in> cball x (b x)"
         using y unfolding mem_cball dist_norm by auto
-      moreover from \<open>x\<in>t\<close> 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
+      moreover have "x \<in> S"
+        using \<open>x\<in>T\<close> \<open>T\<subseteq>S\<close> by auto
+      ultimately have "x + (y - ?a) \<in> S"
+        using y b by blast
     }
     moreover
-    have *: "inj_on (\<lambda>v. v + (y - a)) t"
+    have *: "inj_on (\<lambda>v. v + (y - ?a)) T"
       unfolding inj_on_def by auto
-    have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1"
-      unfolding sum.reindex[OF *] o_def using obt(4) by auto
-    moreover have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a)) *\<^sub>R v) = y"
-      unfolding sum.reindex[OF *] o_def using obt(4,5)
+    have "(\<Sum>v\<in>(\<lambda>v. v + (y - ?a)) ` T. u (v - (y - ?a)) *\<^sub>R v) = y"
+      unfolding sum.reindex[OF *] o_def using obt(4)
       by (simp add: sum.distrib sum_subtractf scaleR_left.sum[symmetric] scaleR_right_distrib)
-    ultimately
-    show "\<exists>sa u. finite sa \<and> (\<forall>x\<in>sa. x \<in> s) \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> sum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = y"
-      apply (rule_tac x="(\<lambda>v. v + (y - a)) ` t" in exI)
-      apply (rule_tac x="\<lambda>v. u (v - (y - a))" in exI)
-      using obt(1, 3)
-      apply auto
-      done
+    ultimately show "y \<in> {y. ?\<Phi> y}"
+    proof (intro CollectI exI conjI)
+      show "finite ((\<lambda>v. v + (y - ?a)) ` T)"
+        by (simp add: obt(1))
+      show "sum (\<lambda>v. u (v - (y - ?a))) ((\<lambda>v. v + (y - ?a)) ` T) = 1"
+        unfolding sum.reindex[OF *] o_def using obt(4) by auto
+    qed (use obt(1, 3) in auto)
   qed
 qed
 
 lemma compact_convex_combinations:
-  fixes s t :: "'a::real_normed_vector set"
-  assumes "compact s" "compact t"
-  shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
+  fixes S T :: "'a::real_normed_vector set"
+  assumes "compact S" "compact T"
+  shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> S \<and> y \<in> T}"
 proof -
-  let ?X = "{0..1} \<times> s \<times> t"
+  let ?X = "{0..1} \<times> S \<times> T"
   let ?h = "(\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
-  have *: "{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t} = ?h ` ?X"
-    apply (rule set_eqI)
-    unfolding image_iff mem_Collect_eq
-    apply rule
-    apply auto
-    apply (rule_tac x=u in rev_bexI, simp)
-    apply (erule rev_bexI)
-    apply (erule rev_bexI, simp)
-    apply auto
-    done
+  have *: "{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> S \<and> y \<in> T} = ?h ` ?X"
+    by force
   have "continuous_on ?X (\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
     unfolding continuous_on by (rule ballI) (intro tendsto_intros)
-  then show ?thesis
-    unfolding *
-    apply (rule compact_continuous_image)
-    apply (intro compact_Times compact_Icc assms)
-    done
+  with assms show ?thesis
+    by (simp add: * compact_Times compact_continuous_image)
 qed
 
 lemma finite_imp_compact_convex_hull:
-  fixes s :: "'a::real_normed_vector set"
-  assumes "finite s"
-  shows "compact (convex hull s)"
-proof (cases "s = {}")
+  fixes S :: "'a::real_normed_vector set"
+  assumes "finite S"
+  shows "compact (convex hull S)"
+proof (cases "S = {}")
   case True
   then show ?thesis by simp
 next
@@ -5029,20 +4994,20 @@
 qed
 
 lemma compact_convex_hull:
-  fixes s :: "'a::euclidean_space set"
-  assumes "compact s"
-  shows "compact (convex hull s)"
-proof (cases "s = {}")
+  fixes S :: "'a::euclidean_space set"
+  assumes "compact S"
+  shows "compact (convex hull S)"
+proof (cases "S = {}")
   case True
   then show ?thesis using compact_empty by simp
 next
   case False
-  then obtain w where "w \<in> s" by auto
+  then obtain w where "w \<in> S" by auto
   show ?thesis
-    unfolding caratheodory[of s]
+    unfolding caratheodory[of S]
   proof (induct ("DIM('a) + 1"))
     case 0
-    have *: "{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
+    have *: "{x.\<exists>sa. finite sa \<and> sa \<subseteq> S \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
       using compact_empty by auto
     from 0 show ?case unfolding * by simp
   next
@@ -5050,27 +5015,27 @@
     show ?case
     proof (cases "n = 0")
       case True
-      have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s"
+      have "{x. \<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T} = S"
         unfolding set_eq_iff and mem_Collect_eq
       proof (rule, rule)
         fix x
-        assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
-        then obtain t where t: "finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t"
+        assume "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
+        then obtain T where T: "finite T" "T \<subseteq> S" "card T \<le> Suc n" "x \<in> convex hull T"
           by auto
-        show "x \<in> s"
-        proof (cases "card t = 0")
+        show "x \<in> S"
+        proof (cases "card T = 0")
           case True
           then show ?thesis
-            using t(4) unfolding card_0_eq[OF t(1)] by simp
+            using T(4) unfolding card_0_eq[OF T(1)] by simp
         next
           case False
-          then have "card t = Suc 0" using t(3) \<open>n=0\<close> by auto
-          then obtain a where "t = {a}" unfolding card_Suc_eq by auto
-          then show ?thesis using t(2,4) by simp
+          then have "card T = Suc 0" using T(3) \<open>n=0\<close> by auto
+          then obtain a where "T = {a}" unfolding card_Suc_eq by auto
+          then show ?thesis using T(2,4) by simp
         qed
       next
-        fix x assume "x\<in>s"
-        then show "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
+        fix x assume "x\<in>S"
+        then show "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
           apply (rule_tac x="{x}" in exI)
           unfolding convex_hull_singleton
           apply auto
@@ -5079,56 +5044,56 @@
       then show ?thesis using assms by simp
     next
       case False
-      have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} =
+      have "{x. \<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T} =
         {(1 - u) *\<^sub>R x + u *\<^sub>R y | x y u.
-          0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> {x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> x \<in> convex hull t}}"
+          0 \<le> u \<and> u \<le> 1 \<and> x \<in> S \<and> y \<in> {x. \<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> n \<and> x \<in> convex hull T}}"
         unfolding set_eq_iff and mem_Collect_eq
       proof (rule, rule)
         fix x
         assume "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
-          0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
-        then obtain u v c t where obt: "x = (1 - c) *\<^sub>R u + c *\<^sub>R v"
-          "0 \<le> c \<and> c \<le> 1" "u \<in> s" "finite t" "t \<subseteq> s" "card t \<le> n"  "v \<in> convex hull t"
+          0 \<le> c \<and> c \<le> 1 \<and> u \<in> S \<and> (\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> n \<and> v \<in> convex hull T)"
+        then obtain u v c T where obt: "x = (1 - c) *\<^sub>R u + c *\<^sub>R v"
+          "0 \<le> c \<and> c \<le> 1" "u \<in> S" "finite T" "T \<subseteq> S" "card T \<le> n"  "v \<in> convex hull T"
           by auto
-        moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u t"
+        moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u T"
           apply (rule convexD_alt)
-          using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex]
-          using obt(7) and hull_mono[of t "insert u t"]
+          using obt(2) and convex_convex_hull and hull_subset[of "insert u T" convex]
+          using obt(7) and hull_mono[of T "insert u T"]
           apply auto
           done
-        ultimately show "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
-          apply (rule_tac x="insert u t" in exI)
+        ultimately show "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
+          apply (rule_tac x="insert u T" in exI)
           apply (auto simp: card_insert_if)
           done
       next
         fix x
-        assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
-        then obtain t where t: "finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t"
+        assume "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
+        then obtain T where T: "finite T" "T \<subseteq> S" "card T \<le> Suc n" "x \<in> convex hull T"
           by auto
         show "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
-          0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
-        proof (cases "card t = Suc n")
+          0 \<le> c \<and> c \<le> 1 \<and> u \<in> S \<and> (\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> n \<and> v \<in> convex hull T)"
+        proof (cases "card T = Suc n")
           case False
-          then have "card t \<le> n" using t(3) by auto
+          then have "card T \<le> n" using T(3) by auto
           then show ?thesis
             apply (rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI)
-            using \<open>w\<in>s\<close> and t
-            apply (auto intro!: exI[where x=t])
+            using \<open>w\<in>S\<close> and T
+            apply (auto intro!: exI[where x=T])
             done
         next
           case True
-          then obtain a u where au: "t = insert a u" "a\<notin>u"
+          then obtain a u where au: "T = insert a u" "a\<notin>u"
             apply (drule_tac card_eq_SucD, auto)
             done
           show ?thesis
           proof (cases "u = {}")
             case True
-            then have "x = a" using t(4)[unfolded au] by auto
+            then have "x = a" using T(4)[unfolded au] by auto
             show ?thesis unfolding \<open>x = a\<close>
               apply (rule_tac x=a in exI)
               apply (rule_tac x=a in exI)
               apply (rule_tac x=1 in exI)
-              using t and \<open>n \<noteq> 0\<close>
+              using T and \<open>n \<noteq> 0\<close>
               unfolding au
               apply (auto intro!: exI[where x="{a}"])
               done
@@ -5136,14 +5101,14 @@
             case False
             obtain ux vx b where obt: "ux\<ge>0" "vx\<ge>0" "ux + vx = 1"
               "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b"
-              using t(4)[unfolded au convex_hull_insert[OF False]]
+              using T(4)[unfolded au convex_hull_insert[OF False]]
               by auto
             have *: "1 - vx = ux" using obt(3) by auto
             show ?thesis
               apply (rule_tac x=a in exI)
               apply (rule_tac x=b in exI)
               apply (rule_tac x=vx in exI)
-              using obt and t(1-3)
+              using obt and T(1-3)
               unfolding au and * using card_insert_disjoint[OF _ au(2)]
               apply (auto intro!: exI[where x=u])
               done
@@ -5195,25 +5160,25 @@
   using dist_increases_online[of d a 0] unfolding dist_norm by auto
 
 lemma simplex_furthest_lt:
-  fixes s :: "'a::real_inner set"
-  assumes "finite s"
-  shows "\<forall>x \<in> convex hull s.  x \<notin> s \<longrightarrow> (\<exists>y \<in> convex hull s. norm (x - a) < norm(y - a))"
+  fixes S :: "'a::real_inner set"
+  assumes "finite S"
+  shows "\<forall>x \<in> convex hull S.  x \<notin> S \<longrightarrow> (\<exists>y \<in> convex hull S. norm (x - a) < norm(y - a))"
   using assms
 proof induct
-  fix x s
-  assume as: "finite s" "x\<notin>s" "\<forall>x\<in>convex hull s. x \<notin> s \<longrightarrow> (\<exists>y\<in>convex hull s. norm (x - a) < norm (y - a))"
-  show "\<forall>xa\<in>convex hull insert x s. xa \<notin> insert x s \<longrightarrow>
-    (\<exists>y\<in>convex hull insert x s. norm (xa - a) < norm (y - a))"
-  proof (rule, rule, cases "s = {}")
+  fix x S
+  assume as: "finite S" "x\<notin>S" "\<forall>x\<in>convex hull S. x \<notin> S \<longrightarrow> (\<exists>y\<in>convex hull S. norm (x - a) < norm (y - a))"
+  show "\<forall>xa\<in>convex hull insert x S. xa \<notin> insert x S \<longrightarrow>
+    (\<exists>y\<in>convex hull insert x S. norm (xa - a) < norm (y - a))"
+  proof (intro impI ballI, cases "S = {}")
     case False
     fix y
-    assume y: "y \<in> convex hull insert x s" "y \<notin> insert x s"
-    obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "y = u *\<^sub>R x + v *\<^sub>R b"
+    assume y: "y \<in> convex hull insert x S" "y \<notin> insert x S"
+    obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull S" "y = u *\<^sub>R x + v *\<^sub>R b"
       using y(1)[unfolded convex_hull_insert[OF False]] by auto
-    show "\<exists>z\<in>convex hull insert x s. norm (y - a) < norm (z - a)"
-    proof (cases "y \<in> convex hull s")
+    show "\<exists>z\<in>convex hull insert x S. norm (y - a) < norm (z - a)"
+    proof (cases "y \<in> convex hull S")
       case True
-      then obtain z where "z \<in> convex hull s" "norm (y - a) < norm (z - a)"
+      then obtain z where "z \<in> convex hull S" "norm (y - a) < norm (z - a)"
         using as(3)[THEN bspec[where x=y]] and y(2) by auto
       then show ?thesis
         apply (rule_tac x=z in bexI)
@@ -5252,14 +5217,12 @@
             unfolding dist_commute[of a]
             unfolding dist_norm obt(5)
             by (simp add: algebra_simps)
-          moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \<in> convex hull insert x s"
-            unfolding convex_hull_insert[OF \<open>s\<noteq>{}\<close>] and mem_Collect_eq
-            apply (rule_tac x="u + w" in exI, rule)
-            defer
-            apply (rule_tac x="v - w" in exI)
-            using \<open>u \<ge> 0\<close> and w and obt(3,4)
-            apply auto
-            done
+          moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \<in> convex hull insert x S"
+            unfolding convex_hull_insert[OF \<open>S\<noteq>{}\<close>]
+          proof (intro CollectI conjI exI)
+            show "u + w \<ge> 0" "v - w \<ge> 0"
+              using obt(1) w by auto
+          qed (use obt in auto)
           ultimately show ?thesis by auto
         next
           assume "dist a y < dist a (y - w *\<^sub>R (x - b))"
@@ -5267,14 +5230,12 @@
             unfolding dist_commute[of a]
             unfolding dist_norm obt(5)
             by (simp add: algebra_simps)
-          moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x s"
-            unfolding convex_hull_insert[OF \<open>s\<noteq>{}\<close>] and mem_Collect_eq
-            apply (rule_tac x="u - w" in exI, rule)
-            defer
-            apply (rule_tac x="v + w" in exI)
-            using \<open>u \<ge> 0\<close> and w and obt(3,4)
-            apply auto
-            done
+          moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x S"
+            unfolding convex_hull_insert[OF \<open>S\<noteq>{}\<close>]
+          proof (intro CollectI conjI exI)
+            show "u - w \<ge> 0" "v + w \<ge> 0"
+              using obt(1) w by auto
+          qed (use obt in auto)
           ultimately show ?thesis by auto
         qed
       qed auto
@@ -5283,22 +5244,22 @@
 qed (auto simp: assms)
 
 lemma simplex_furthest_le:
-  fixes s :: "'a::real_inner set"
-  assumes "finite s"
-    and "s \<noteq> {}"
-  shows "\<exists>y\<in>s. \<forall>x\<in> convex hull s. norm (x - a) \<le> norm (y - a)"
+  fixes S :: "'a::real_inner set"
+  assumes "finite S"
+    and "S \<noteq> {}"
+  shows "\<exists>y\<in>S. \<forall>x\<in> convex hull S. norm (x - a) \<le> norm (y - a)"
 proof -
-  have "convex hull s \<noteq> {}"
-    using hull_subset[of s convex] and assms(2) by auto
-  then obtain x where x: "x \<in> convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
-    using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
+  have "convex hull S \<noteq> {}"
+    using hull_subset[of S convex] and assms(2) by auto
+  then obtain x where x: "x \<in> convex hull S" "\<forall>y\<in>convex hull S. norm (y - a) \<le> norm (x - a)"
+    using distance_attains_sup[OF finite_imp_compact_convex_hull[OF \<open>finite S\<close>], of a]
     unfolding dist_commute[of a]
     unfolding dist_norm
     by auto
   show ?thesis
-  proof (cases "x \<in> s")
+  proof (cases "x \<in> S")
     case False
-    then obtain y where "y \<in> convex hull s" "norm (x - a) < norm (y - a)"
+    then obtain y where "y \<in> convex hull S" "norm (x - a) < norm (y - a)"
       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1)
       by auto
     then show ?thesis
@@ -5310,34 +5271,34 @@
 qed
 
 lemma simplex_furthest_le_exists:
-  fixes s :: "('a::real_inner) set"
-  shows "finite s \<Longrightarrow> \<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm (x - a) \<le> norm (y - a)"
-  using simplex_furthest_le[of s] by (cases "s = {}") auto
+  fixes S :: "('a::real_inner) set"
+  shows "finite S \<Longrightarrow> \<forall>x\<in>(convex hull S). \<exists>y\<in>S. norm (x - a) \<le> norm (y - a)"
+  using simplex_furthest_le[of S] by (cases "S = {}") auto
 
 lemma simplex_extremal_le:
-  fixes s :: "'a::real_inner set"
-  assumes "finite s"
-    and "s \<noteq> {}"
-  shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm (x - y) \<le> norm (u - v)"
+  fixes S :: "'a::real_inner set"
+  assumes "finite S"
+    and "S \<noteq> {}"
+  shows "\<exists>u\<in>S. \<exists>v\<in>S. \<forall>x\<in>convex hull S. \<forall>y \<in> convex hull S. norm (x - y) \<le> norm (u - v)"
 proof -
-  have "convex hull s \<noteq> {}"
-    using hull_subset[of s convex] and assms(2) by auto
-  then obtain u v where obt: "u \<in> convex hull s" "v \<in> convex hull s"
-    "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull s. norm (x - y) \<le> norm (u - v)"
+  have "convex hull S \<noteq> {}"
+    using hull_subset[of S convex] and assms(2) by auto
+  then obtain u v where obt: "u \<in> convex hull S" "v \<in> convex hull S"
+    "\<forall>x\<in>convex hull S. \<forall>y\<in>convex hull S. norm (x - y) \<le> norm (u - v)"
     using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]]
     by (auto simp: dist_norm)
   then show ?thesis
-  proof (cases "u\<notin>s \<or> v\<notin>s", elim disjE)
-    assume "u \<notin> s"
-    then obtain y where "y \<in> convex hull s" "norm (u - v) < norm (y - v)"
+  proof (cases "u\<notin>S \<or> v\<notin>S", elim disjE)
+    assume "u \<notin> S"
+    then obtain y where "y \<in> convex hull S" "norm (u - v) < norm (y - v)"
       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1)
       by auto
     then show ?thesis
       using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2)
       by auto
   next
-    assume "v \<notin> s"
-    then obtain y where "y \<in> convex hull s" "norm (v - u) < norm (y - u)"
+    assume "v \<notin> S"
+    then obtain y where "y \<in> convex hull S" "norm (v - u) < norm (y - u)"
       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2)
       by auto
     then show ?thesis
@@ -5347,45 +5308,45 @@
 qed
 
 lemma simplex_extremal_le_exists:
-  fixes s :: "'a::real_inner set"
-  shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s \<Longrightarrow>
-    \<exists>u\<in>s. \<exists>v\<in>s. norm (x - y) \<le> norm (u - v)"
-  using convex_hull_empty simplex_extremal_le[of s]
-  by(cases "s = {}") auto
+  fixes S :: "'a::real_inner set"
+  shows "finite S \<Longrightarrow> x \<in> convex hull S \<Longrightarrow> y \<in> convex hull S \<Longrightarrow>
+    \<exists>u\<in>S. \<exists>v\<in>S. norm (x - y) \<le> norm (u - v)"
+  using convex_hull_empty simplex_extremal_le[of S]
+  by(cases "S = {}") auto
 
 
 subsection \<open>Closest point of a convex set is unique, with a continuous projection\<close>
 
 definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
-  where "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
+  where "closest_point S a = (SOME x. x \<in> S \<and> (\<forall>y\<in>S. dist a x \<le> dist a y))"
 
 lemma closest_point_exists:
-  assumes "closed s"
-    and "s \<noteq> {}"
-  shows "closest_point s a \<in> s"
-    and "\<forall>y\<in>s. dist a (closest_point s a) \<le> dist a y"
+  assumes "closed S"
+    and "S \<noteq> {}"
+  shows "closest_point S a \<in> S"
+    and "\<forall>y\<in>S. dist a (closest_point S a) \<le> dist a y"
   unfolding closest_point_def
   apply(rule_tac[!] someI2_ex)
   apply (auto intro: distance_attains_inf[OF assms(1,2), of a])
   done
 
-lemma closest_point_in_set: "closed s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> closest_point s a \<in> s"
+lemma closest_point_in_set: "closed S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> closest_point S a \<in> S"
   by (meson closest_point_exists)
 
-lemma closest_point_le: "closed s \<Longrightarrow> x \<in> s \<Longrightarrow> dist a (closest_point s a) \<le> dist a x"
-  using closest_point_exists[of s] by auto
+lemma closest_point_le: "closed S \<Longrightarrow> x \<in> S \<Longrightarrow> dist a (closest_point S a) \<le> dist a x"
+  using closest_point_exists[of S] by auto
 
 lemma closest_point_self:
-  assumes "x \<in> s"
-  shows "closest_point s x = x"
+  assumes "x \<in> S"
+  shows "closest_point S x = x"
   unfolding closest_point_def
   apply (rule some1_equality, rule ex1I[of _ x])
   using assms
   apply auto
   done
 
-lemma closest_point_refl: "closed s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> closest_point s x = x \<longleftrightarrow> x \<in> s"
-  using closest_point_in_set[of s x] closest_point_self[of x s]
+lemma closest_point_refl: "closed S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> closest_point S x = x \<longleftrightarrow> x \<in> S"
+  using closest_point_in_set[of S x] closest_point_self[of x S]
   by auto
 
 lemma closer_points_lemma:
@@ -5417,14 +5378,14 @@
 qed
 
 lemma any_closest_point_dot:
-  assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
+  assumes "convex S" "closed S" "x \<in> S" "y \<in> S" "\<forall>z\<in>S. dist a x \<le> dist a z"
   shows "inner (a - x) (y - x) \<le> 0"
 proof (rule ccontr)
   assume "\<not> ?thesis"
   then obtain u where u: "u>0" "u\<le>1" "dist (x + u *\<^sub>R (y - x)) a < dist x a"
     using closer_point_lemma[of a x y] by auto
   let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y"
-  have "?z \<in> s"
+  have "?z \<in> S"
     using convexD_alt[OF assms(1,3,4), of u] using u by auto
   then show False
     using assms(5)[THEN bspec[where x="?z"]] and u(3)
@@ -5433,30 +5394,30 @@
 
 lemma any_closest_point_unique:
   fixes x :: "'a::real_inner"
-  assumes "convex s" "closed s" "x \<in> s" "y \<in> s"
-    "\<forall>z\<in>s. dist a x \<le> dist a z" "\<forall>z\<in>s. dist a y \<le> dist a z"
+  assumes "convex S" "closed S" "x \<in> S" "y \<in> S"
+    "\<forall>z\<in>S. dist a x \<le> dist a z" "\<forall>z\<in>S. dist a y \<le> dist a z"
   shows "x = y"
   using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
   unfolding norm_pths(1) and norm_le_square
   by (auto simp: algebra_simps)
 
 lemma closest_point_unique:
-  assumes "convex s" "closed s" "x \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
-  shows "x = closest_point s a"
-  using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point s a"]
+  assumes "convex S" "closed S" "x \<in> S" "\<forall>z\<in>S. dist a x \<le> dist a z"
+  shows "x = closest_point S a"
+  using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point S a"]
   using closest_point_exists[OF assms(2)] and assms(3) by auto
 
 lemma closest_point_dot:
-  assumes "convex s" "closed s" "x \<in> s"
-  shows "inner (a - closest_point s a) (x - closest_point s a) \<le> 0"
+  assumes "convex S" "closed S" "x \<in> S"
+  shows "inner (a - closest_point S a) (x - closest_point S a) \<le> 0"
   apply (rule any_closest_point_dot[OF assms(1,2) _ assms(3)])
   using closest_point_exists[OF assms(2)] and assms(3)
   apply auto
   done
 
 lemma closest_point_lt:
-  assumes "convex s" "closed s" "x \<in> s" "x \<noteq> closest_point s a"
-  shows "dist a (closest_point s a) < dist a x"
+  assumes "convex S" "closed S" "x \<in> S" "x \<noteq> closest_point S a"
+  shows "dist a (closest_point S a) < dist a x"
   apply (rule ccontr)
   apply (rule_tac notE[OF assms(4)])
   apply (rule closest_point_unique[OF assms(1-3), of a])
@@ -5465,34 +5426,34 @@
   done
 
 lemma closest_point_lipschitz:
-  assumes "convex s"
-    and "closed s" "s \<noteq> {}"
-  shows "dist (closest_point s x) (closest_point s y) \<le> dist x y"
+  assumes "convex S"
+    and "closed S" "S \<noteq> {}"
+  shows "dist (closest_point S x) (closest_point S y) \<le> dist x y"
 proof -
-  have "inner (x - closest_point s x) (closest_point s y - closest_point s x) \<le> 0"
-    and "inner (y - closest_point s y) (closest_point s x - closest_point s y) \<le> 0"
+  have "inner (x - closest_point S x) (closest_point S y - closest_point S x) \<le> 0"
+    and "inner (y - closest_point S y) (closest_point S x - closest_point S y) \<le> 0"
     apply (rule_tac[!] any_closest_point_dot[OF assms(1-2)])
     using closest_point_exists[OF assms(2-3)]
     apply auto
     done
   then show ?thesis unfolding dist_norm and norm_le
-    using inner_ge_zero[of "(x - closest_point s x) - (y - closest_point s y)"]
+    using inner_ge_zero[of "(x - closest_point S x) - (y - closest_point S y)"]
     by (simp add: inner_add inner_diff inner_commute)
 qed
 
 lemma continuous_at_closest_point:
-  assumes "convex s"
-    and "closed s"
-    and "s \<noteq> {}"
-  shows "continuous (at x) (closest_point s)"
+  assumes "convex S"
+    and "closed S"
+    and "S \<noteq> {}"
+  shows "continuous (at x) (closest_point S)"
   unfolding continuous_at_eps_delta
   using le_less_trans[OF closest_point_lipschitz[OF assms]] by auto
 
 lemma continuous_on_closest_point:
-  assumes "convex s"
-    and "closed s"
-    and "s \<noteq> {}"
-  shows "continuous_on t (closest_point s)"
+  assumes "convex S"
+    and "closed S"
+    and "S \<noteq> {}"
+  shows "continuous_on t (closest_point S)"
   by (metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms])
 
 proposition closest_point_in_rel_interior:
@@ -5543,119 +5504,84 @@
 
 lemma supporting_hyperplane_closed_point:
   fixes z :: "'a::{real_inner,heine_borel}"
-  assumes "convex s"
-    and "closed s"
-    and "s \<noteq> {}"
-    and "z \<notin> s"
-  shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> inner a y = b \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
+  assumes "convex S"
+    and "closed S"
+    and "S \<noteq> {}"
+    and "z \<notin> S"
+  shows "\<exists>a b. \<exists>y\<in>S. inner a z < b \<and> inner a y = b \<and> (\<forall>x\<in>S. inner a x \<ge> b)"
 proof -
-  obtain y where "y \<in> s" and y: "\<forall>x\<in>s. dist z y \<le> dist z x"
+  obtain y where "y \<in> S" and y: "\<forall>x\<in>S. dist z y \<le> dist z x"
     by (metis distance_attains_inf[OF assms(2-3)])
   show ?thesis
-    apply (rule_tac x="y - z" in exI)
-    apply (rule_tac x="inner (y - z) y" in exI)
-    apply (rule_tac x=y in bexI, rule)
-    defer
-    apply rule
-    defer
-    apply rule
-    apply (rule ccontr)
-    using \<open>y \<in> s\<close>
-  proof -
-    show "inner (y - z) z < inner (y - z) y"
-      apply (subst diff_gt_0_iff_gt [symmetric])
-      unfolding inner_diff_right[symmetric] and inner_gt_zero_iff
-      using \<open>y\<in>s\<close> \<open>z\<notin>s\<close>
-      apply auto
-      done
-  next
-    fix x
-    assume "x \<in> s"
-    have *: "\<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> dist z y \<le> dist z ((1 - u) *\<^sub>R y + u *\<^sub>R x)"
-      using assms(1)[unfolded convex_alt] and y and \<open>x\<in>s\<close> and \<open>y\<in>s\<close> by auto
-    assume "\<not> inner (y - z) y \<le> inner (y - z) x"
-    then obtain v where "v > 0" "v \<le> 1" "dist (y + v *\<^sub>R (x - y)) z < dist y z"
-      using closer_point_lemma[of z y x] by (auto simp: inner_diff)
-    then show False
-      using *[THEN spec[where x=v]] by (auto simp: dist_commute algebra_simps)
-  qed auto
+  proof (intro exI bexI conjI ballI)
+    show "(y - z) \<bullet> z < (y - z) \<bullet> y"
+      by (metis \<open>y \<in> S\<close> assms(4) diff_gt_0_iff_gt inner_commute inner_diff_left inner_gt_zero_iff right_minus_eq)
+    show "(y - z) \<bullet> y \<le> (y - z) \<bullet> x" if "x \<in> S" for x
+    proof (rule ccontr)
+      have *: "\<And>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> dist z y \<le> dist z ((1 - u) *\<^sub>R y + u *\<^sub>R x)"
+        using assms(1)[unfolded convex_alt] and y and \<open>x\<in>S\<close> and \<open>y\<in>S\<close> by auto
+      assume "\<not> (y - z) \<bullet> y \<le> (y - z) \<bullet> x"
+      then obtain v where "v > 0" "v \<le> 1" "dist (y + v *\<^sub>R (x - y)) z < dist y z"
+        using closer_point_lemma[of z y x] by (auto simp: inner_diff)
+      then show False
+        using *[of v] by (auto simp: dist_commute algebra_simps)
+    qed
+  qed (use \<open>y \<in> S\<close> in auto)
 qed
 
 lemma separating_hyperplane_closed_point:
   fixes z :: "'a::{real_inner,heine_borel}"
-  assumes "convex s"
-    and "closed s"
-    and "z \<notin> s"
-  shows "\<exists>a b. inner a z < b \<and> (\<forall>x\<in>s. inner a x > b)"
-proof (cases "s = {}")
+  assumes "convex S"
+    and "closed S"
+    and "z \<notin> S"
+  shows "\<exists>a b. inner a z < b \<and> (\<forall>x\<in>S. inner a x > b)"
+proof (cases "S = {}")
   case True
   then show ?thesis
-    apply (rule_tac x="-z" in exI)
-    apply (rule_tac x=1 in exI)
-    using less_le_trans[OF _ inner_ge_zero[of z]]
-    apply auto
-    done
+    by (simp add: gt_ex)
 next
   case False
-  obtain y where "y \<in> s" and y: "\<forall>x\<in>s. dist z y \<le> dist z x"
+  obtain y where "y \<in> S" and y: "\<And>x. x \<in> S \<Longrightarrow> dist z y \<le> dist z x"
     by (metis distance_attains_inf[OF assms(2) False])
   show ?thesis
-    apply (rule_tac x="y - z" in exI)
-    apply (rule_tac x="inner (y - z) z + (norm (y - z))\<^sup>2 / 2" in exI)
-    apply rule
-    defer
-    apply rule
-  proof -
+  proof (intro exI conjI ballI)
+    show "(y - z) \<bullet> z < inner (y - z) z + (norm (y - z))\<^sup>2 / 2"
+      using \<open>y\<in>S\<close> \<open>z\<notin>S\<close> by auto
+  next
     fix x
-    assume "x \<in> s"
-    have "\<not> 0 < inner (z - y) (x - y)"
-      apply (rule notI)
-      apply (drule closer_point_lemma)
+    assume "x \<in> S"
+    have "False" if *: "0 < inner (z - y) (x - y)"
     proof -
-      assume "\<exists>u>0. u \<le> 1 \<and> dist (y + u *\<^sub>R (x - y)) z < dist y z"
-      then obtain u where "u > 0" "u \<le> 1" "dist (y + u *\<^sub>R (x - y)) z < dist y z"
-        by auto
-      then show False using y[THEN bspec[where x="y + u *\<^sub>R (x - y)"]]
-        using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
-        using \<open>x\<in>s\<close> \<open>y\<in>s\<close> by (auto simp: dist_commute algebra_simps)
+      obtain u where "u > 0" "u \<le> 1" "dist (y + u *\<^sub>R (x - y)) z < dist y z"
+        using * closer_point_lemma by blast
+      then show False using y[of "y + u *\<^sub>R (x - y)"] convexD_alt [OF \<open>convex S\<close>]
+        using \<open>x\<in>S\<close> \<open>y\<in>S\<close> by (auto simp: dist_commute algebra_simps)
     qed
     moreover have "0 < (norm (y - z))\<^sup>2"
-      using \<open>y\<in>s\<close> \<open>z\<notin>s\<close> by auto
+      using \<open>y\<in>S\<close> \<open>z\<notin>S\<close> by auto
     then have "0 < inner (y - z) (y - z)"
       unfolding power2_norm_eq_inner by simp
-    ultimately show "inner (y - z) z + (norm (y - z))\<^sup>2 / 2 < inner (y - z) x"
-      unfolding power2_norm_eq_inner and not_less
-      by (auto simp: field_simps inner_commute inner_diff)
-  qed (insert \<open>y\<in>s\<close> \<open>z\<notin>s\<close>, auto)
+    ultimately show "(y - z) \<bullet> z + (norm (y - z))\<^sup>2 / 2 < (y - z) \<bullet> x"
+      by (force simp: field_simps power2_norm_eq_inner inner_commute inner_diff)
+  qed 
 qed
 
 lemma separating_hyperplane_closed_0:
-  assumes "convex (s::('a::euclidean_space) set)"
-    and "closed s"
-    and "0 \<notin> s"
-  shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>s. inner a x > b)"
-proof (cases "s = {}")
+  assumes "convex (S::('a::euclidean_space) set)"
+    and "closed S"
+    and "0 \<notin> S"
+  shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>S. inner a x > b)"
+proof (cases "S = {}")
   case True
-  have "norm ((SOME i. i\<in>Basis)::'a) = 1" "(SOME i. i\<in>Basis) \<noteq> (0::'a)"
-    defer
-    apply (subst norm_le_zero_iff[symmetric])
-    apply (auto simp: SOME_Basis)
-    done
+  have "(SOME i. i\<in>Basis) \<noteq> (0::'a)"
+    by (metis Basis_zero SOME_Basis)
   then show ?thesis
-    apply (rule_tac x="SOME i. i\<in>Basis" in exI)
-    apply (rule_tac x=1 in exI)
-    using True using DIM_positive[where 'a='a]
-    apply auto
-    done
+    using True zero_less_one by blast
 next
   case False
   then show ?thesis
     using False using separating_hyperplane_closed_point[OF assms]
-    apply (elim exE)
-    unfolding inner_zero_right
-    apply (rule_tac x=a in exI)
-    apply (rule_tac x=b in exI, auto)
-    done
+    by (metis all_not_in_conv inner_zero_left inner_zero_right less_eq_real_def not_le)
 qed
 
 
@@ -5826,19 +5752,13 @@
   assumes "convex S"
   shows "convex (interior S)"
   unfolding convex_alt Ball_def mem_interior
-  apply (rule,rule,rule,rule,rule,rule)
-  apply (elim exE conjE)
-proof -
+proof clarify
   fix x y u
   assume u: "0 \<le> u" "u \<le> (1::real)"
   fix e d
   assume ed: "ball x e \<subseteq> S" "ball y d \<subseteq> S" "0<d" "0<e"
   show "\<exists>e>0. ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) e \<subseteq> S"
-    apply (rule_tac x="min d e" in exI, rule)
-    unfolding subset_eq
-    defer
-    apply rule
-  proof -
+  proof (intro exI conjI subsetI)
     fix z
     assume "z \<in> ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) (min d e)"
     then have "(1- u) *\<^sub>R (z - u *\<^sub>R (y - x)) + u *\<^sub>R (z + (1 - u) *\<^sub>R (y - x)) \<in> S"
@@ -6129,7 +6049,7 @@
     and "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
   shows "\<Inter>f \<noteq> {}"
   using assms
-proof (induct n arbitrary: f)
+proof (induction n arbitrary: f)
   case 0
   then show ?case by auto
 next
@@ -6137,45 +6057,39 @@
   have "finite f"
     using \<open>card f = Suc n\<close> by (auto intro: card_ge_0_finite)
   show "\<Inter>f \<noteq> {}"
-    apply (cases "n = DIM('a)")
-    apply (rule Suc(5)[rule_format])
-    unfolding \<open>card f = Suc n\<close>
-  proof -
-    assume ng: "n \<noteq> DIM('a)"
-    then have "\<exists>X. \<forall>s\<in>f. X s \<in> \<Inter>(f - {s})"
-      apply (rule_tac bchoice)
-      unfolding ex_in_conv
-      apply (rule, rule Suc(1)[rule_format])
-      unfolding card_Diff_singleton_if[OF \<open>finite f\<close>] \<open>card f = Suc n\<close>
-      defer
-      defer
-      apply (rule Suc(4)[rule_format])
-      defer
-      apply (rule Suc(5)[rule_format])
-      using Suc(3) \<open>finite f\<close>
-      apply auto
-      done
-    then obtain X where X: "\<forall>s\<in>f. X s \<in> \<Inter>(f - {s})" by auto
+  proof (cases "n = DIM('a)")
+    case True
+    then show ?thesis
+      by (simp add: Suc.prems(1) Suc.prems(4))
+  next
+    case False
+    have "\<Inter>(f - {s}) \<noteq> {}" if "s \<in> f" for s
+    proof (rule Suc.IH[rule_format])
+      show "card (f - {s}) = n"
+        by (simp add: Suc.prems(1) \<open>finite f\<close> that)
+      show "DIM('a) + 1 \<le> n"
+        using False Suc.prems(2) by linarith
+      show "\<And>t. \<lbrakk>t \<subseteq> f - {s}; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
+        by (simp add: Suc.prems(4) subset_Diff_insert)
+    qed (use Suc in auto)
+    then have "\<forall>s\<in>f. \<exists>x. x \<in> \<Inter>(f - {s})"
+      by blast
+    then obtain X where X: "\<And>s. s\<in>f \<Longrightarrow> X s \<in> \<Inter>(f - {s})"
+      by metis
     show ?thesis
     proof (cases "inj_on X f")
       case False
-      then obtain s t where st: "s\<noteq>t" "s\<in>f" "t\<in>f" "X s = X t"
+      then obtain s t where "s\<noteq>t" and st: "s\<in>f" "t\<in>f" "X s = X t"
         unfolding inj_on_def by auto
       then have *: "\<Inter>f = \<Inter>(f - {s}) \<inter> \<Inter>(f - {t})" by auto
       show ?thesis
-        unfolding *
-        unfolding ex_in_conv[symmetric]
-        apply (rule_tac x="X s" in exI, rule)
-        apply (rule X[rule_format])
-        using X st
-        apply auto
-        done
+        by (metis "*" X disjoint_iff_not_equal st)
     next
       case True
       then obtain m p where mp: "m \<inter> p = {}" "m \<union> p = X ` f" "convex hull m \<inter> convex hull p \<noteq> {}"
         using radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"]
         unfolding card_image[OF True] and \<open>card f = Suc n\<close>
-        using Suc(3) \<open>finite f\<close> and ng
+        using Suc(3) \<open>finite f\<close> and False
         by auto
       have "m \<subseteq> X ` f" "p \<subseteq> X ` f"
         using mp(2) by auto
@@ -6192,40 +6106,17 @@
         using inj_on_image_Int[OF True gh(3,4)]
         by auto
       have "convex hull (X ` h) \<subseteq> \<Inter>g" "convex hull (X ` g) \<subseteq> \<Inter>h"
-        apply (rule_tac [!] hull_minimal)
-        using Suc gh(3-4)
-        unfolding subset_eq
-        apply (rule_tac [2] convex_Inter, rule_tac [4] convex_Inter)
-        prefer 3
-        apply rule
-      proof -
-        fix x
-        assume "x \<in> X ` g"
-        then obtain y where "y \<in> g" "x = X y"
-          unfolding image_iff ..
-        then show "x \<in> \<Inter>h"
-          using X[THEN bspec[where x=y]] using * f by auto
-      next
-        show "\<forall>x\<in>X ` h. x \<in> \<Inter>g"
-        proof
-        fix x
-        assume "x \<in> X ` h"
-        then obtain y where "y \<in> h" "x = X y"
-          unfolding image_iff ..
-        then show "x \<in> \<Inter>g"
-          using X[THEN bspec[where x=y]] using * f by auto
-      qed
-      qed auto
+        by (rule hull_minimal; use X * f in \<open>auto simp: Suc.prems(3) convex_Inter\<close>)+
       then show ?thesis
         unfolding f using mp(3)[unfolded gh] by blast
     qed
-  qed auto
+  qed 
 qed
 
 theorem%important helly:
   fixes f :: "'a::euclidean_space set set"
   assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
-    and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
+    and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
   shows "\<Inter>f \<noteq> {}"
   apply%unimportant (rule helly_induct)
   using assms
@@ -6235,70 +6126,76 @@
 
 subsection \<open>Epigraphs of convex functions\<close>
 
-definition%important "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
-
-lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y"
+definition%important "epigraph S (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> S \<and> f (fst xy) \<le> snd xy}"
+
+lemma mem_epigraph: "(x, y) \<in> epigraph S f \<longleftrightarrow> x \<in> S \<and> f x \<le> y"
   unfolding epigraph_def by auto
 
-lemma convex_epigraph: "convex (epigraph s f) \<longleftrightarrow> convex_on s f \<and> convex s"
-  unfolding convex_def convex_on_def
-  unfolding Ball_def split_paired_All epigraph_def
-  unfolding mem_Collect_eq fst_conv snd_conv fst_add snd_add fst_scaleR snd_scaleR Ball_def[symmetric]
-  apply safe
-  defer
-  apply (erule_tac x=x in allE)
-  apply (erule_tac x="f x" in allE, safe)
-  apply (erule_tac x=xa in allE)
-  apply (erule_tac x="f xa" in allE)
-  prefer 3
-  apply (rule_tac y="u * f a + v * f aa" in order_trans)
-  defer
-  apply (auto intro!:mult_left_mono add_mono)
-  done
-
-lemma convex_epigraphI: "convex_on s f \<Longrightarrow> convex s \<Longrightarrow> convex (epigraph s f)"
+lemma convex_epigraph: "convex (epigraph S f) \<longleftrightarrow> convex_on S f \<and> convex S"
+proof safe
+  assume L: "convex (epigraph S f)"
+  then show "convex_on S f"
+    by (auto simp: convex_def convex_on_def epigraph_def)
+  show "convex S"
+    using L
+    apply (clarsimp simp: convex_def convex_on_def epigraph_def)
+    apply (erule_tac x=x in allE)
+    apply (erule_tac x="f x" in allE, safe)
+    apply (erule_tac x=y in allE)
+    apply (erule_tac x="f y" in allE)
+    apply (auto simp: )
+    done
+next
+  assume "convex_on S f" "convex S"
+  then show "convex (epigraph S f)"
+    unfolding convex_def convex_on_def epigraph_def
+    apply safe
+     apply (rule_tac [2] y="u * f a + v * f aa" in order_trans)
+      apply (auto intro!:mult_left_mono add_mono)
+    done
+qed
+
+lemma convex_epigraphI: "convex_on S f \<Longrightarrow> convex S \<Longrightarrow> convex (epigraph S f)"
   unfolding convex_epigraph by auto
 
-lemma convex_epigraph_convex: "convex s \<Longrightarrow> convex_on s f \<longleftrightarrow> convex(epigraph s f)"
+lemma convex_epigraph_convex: "convex S \<Longrightarrow> convex_on S f \<longleftrightarrow> convex(epigraph S f)"
   by (simp add: convex_epigraph)
 
 
 subsubsection%unimportant \<open>Use this to derive general bound property of convex function\<close>
 
 lemma convex_on:
-  assumes "convex s"
-  shows "convex_on s f \<longleftrightarrow>
-    (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> sum u {1..k} = 1 \<longrightarrow>
+  assumes "convex S"
+  shows "convex_on S f \<longleftrightarrow>
+    (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> S) \<and> sum u {1..k} = 1 \<longrightarrow>
       f (sum (\<lambda>i. u i *\<^sub>R x i) {1..k}) \<le> sum (\<lambda>i. u i * f(x i)) {1..k})"
+
   unfolding convex_epigraph_convex[OF assms] convex epigraph_def Ball_def mem_Collect_eq
   unfolding fst_sum snd_sum fst_scaleR snd_scaleR
   apply safe
-  apply (drule_tac x=k in spec)
-  apply (drule_tac x=u in spec)
-  apply (drule_tac x="\<lambda>i. (x i, f (x i))" in spec)
-  apply simp
-  using assms[unfolded convex]
-  apply simp
-  apply (rule_tac y="\<Sum>i = 1..k. u i * f (fst (x i))" in order_trans)
-  defer
-  apply (rule sum_mono)
-  apply (erule_tac x=i in allE)
+    apply (drule_tac x=k in spec)
+    apply (drule_tac x=u in spec)
+    apply (drule_tac x="\<lambda>i. (x i, f (x i))" in spec)
+    apply simp
+  using assms[unfolded convex] apply simp
+  apply (rule_tac y="\<Sum>i = 1..k. u i * f (fst (x i))" in order_trans, force)
+   apply (rule sum_mono)
+   apply (erule_tac x=i in allE)
   unfolding real_scaleR_def
-  apply (rule mult_left_mono)
-  using assms[unfolded convex]
-  apply auto
+   apply (rule mult_left_mono)
+  using assms[unfolded convex] apply auto
   done
 
 
 subsection%unimportant \<open>Convexity of general and special intervals\<close>
 
 lemma is_interval_convex:
-  fixes s :: "'a::euclidean_space set"
-  assumes "is_interval s"
-  shows "convex s"
+  fixes S :: "'a::euclidean_space set"
+  assumes "is_interval S"
+  shows "convex S"
 proof (rule convexI)
   fix x y and u v :: real
-  assume as: "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1"
+  assume as: "x \<in> S" "y \<in> S" "0 \<le> u" "0 \<le> v" "u + v = 1"
   then have *: "u = 1 - v" "1 - v \<ge> 0" and **: "v = 1 - u" "1 - u \<ge> 0"
     by auto
   {
@@ -6331,7 +6228,7 @@
       using **(2) as(3)
       by (auto simp: field_simps intro!:mult_right_mono)
   }
-  ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s"
+  ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> S"
     apply -
     apply (rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
     using as(3-) DIM_positive[where 'a='a]
@@ -6340,8 +6237,8 @@
 qed
 
 lemma is_interval_connected:
-  fixes s :: "'a::euclidean_space set"
-  shows "is_interval s \<Longrightarrow> connected s"
+  fixes S :: "'a::euclidean_space set"
+  shows "is_interval S \<Longrightarrow> connected S"
   using is_interval_convex convex_connected by auto
 
 lemma convex_box [simp]: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))"
@@ -6818,20 +6715,16 @@
         finally have w: "(1 / t) *\<^sub>R w + ((t - 1) / t) *\<^sub>R x = y"
           unfolding w_def using False and \<open>t > 0\<close>
           by (auto simp: algebra_simps)
-        have  "2 * B < e * t"
+        have 2: "2 * B < e * t"
           unfolding t_def using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
           by (auto simp:field_simps)
-        then have "(f w - f x) / t < e"
-          using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>x\<in>s\<close>]
-          using \<open>t > 0\<close> by (auto simp:field_simps)
-        then have th1: "f y - f x < e"
-          apply -
-          apply (rule le_less_trans)
-          defer
-          apply assumption
+        have "f y - f x \<le> (f w - f x) / t"
           using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
           using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> s\<close> \<open>w \<in> s\<close>
           by (auto simp:field_simps)
+        also have "... < e"
+          using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>x\<in>s\<close>] 2 \<open>t > 0\<close> by (auto simp: field_simps)
+        finally have th1: "f y - f x < e" .
       }
       moreover
       {