# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1598453961 -3600
# Node ID a6cbf8ce979e5728c922a7f2a6f2c83a1e1a055a
# Parent  b7d6b9e71f880382265af65c2904b432e46bb894
tiny tidy-up of proofs

diff -r b7d6b9e71f88 -r a6cbf8ce979e src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Tue Aug 25 23:21:38 2020 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Wed Aug 26 15:59:21 2020 +0100
@@ -88,26 +88,24 @@
       by simp
     have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
       using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
-    have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
-      unfolding dist_norm
-      unfolding norm_scaleR[symmetric]
-      apply (rule arg_cong[where f=norm])
+    have "c - ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = (1 / e) *\<^sub>R (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
       using \<open>e > 0\<close>
       by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
+    then have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
+      by (simp add: dist_norm)
     also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
       by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
     also have "\<dots> < d"
       using as[unfolded dist_norm] and \<open>e > 0\<close>
       by (auto simp add:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute)
-    finally show "y \<in> S"
-      apply (subst *)
-      apply (rule assms(1)[unfolded convex_alt,rule_format])
-      apply (rule d[unfolded subset_eq,rule_format])
-      unfolding mem_ball
-      using assms(3-5)
-      apply auto
+    finally have "(1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x \<in> S"
+      using assms(3-5) d
+      apply (intro convexD_alt [OF \<open>convex S\<close>])
+         apply (auto simp: intro: convexD_alt [OF \<open>convex S\<close>])
       done
-  qed (insert \<open>e>0\<close> \<open>d>0\<close>, auto)
+    with \<open>e > 0\<close> show "y \<in> S"
+      by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
+  qed (use \<open>e>0\<close> \<open>d>0\<close> in auto)
 qed
 
 lemma mem_interior_closure_convex_shrink:
@@ -125,10 +123,7 @@
   proof (cases "x \<in> S")
     case True
     then show ?thesis
-      using \<open>e > 0\<close> \<open>d > 0\<close>
-      apply (rule_tac bexI[where x=x])
-      apply (auto)
-      done
+      using \<open>e > 0\<close> \<open>d > 0\<close> by force
   next
     case False
     then have x: "x islimpt S"
@@ -139,23 +134,17 @@
       obtain y where "y \<in> S" "y \<noteq> x" "dist y x < 1"
         using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
       then show ?thesis
-        apply (rule_tac x=y in bexI)
-        unfolding True
-        using \<open>d > 0\<close>
-        apply auto
-        done
+        using True \<open>0 < d\<close> by auto
     next
       case False
       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
         using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by auto
       then obtain y where "y \<in> S" "y \<noteq> x" "dist y x < e * d / (1 - e)"
-        using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
+        using islimpt_approachable x by blast
+      then have "norm (y - x) * (1 - e) < e * d"
+        by (metis "*" dist_norm mult_imp_div_pos_le not_less)
       then show ?thesis
-        apply (rule_tac x=y in bexI)
-        unfolding dist_norm
-        using pos_less_divide_eq[OF *]
-        apply auto
-        done
+        using \<open>y \<in> S\<close> by blast
     qed
   qed
   then obtain y where "y \<in> S" and y: "norm (y - x) * (1 - e) < e * d"
@@ -164,10 +153,12 @@
   have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)"
     unfolding z_def using \<open>e > 0\<close>
     by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
-  have "z \<in> interior S"
-    apply (rule interior_mono[OF d,unfolded subset_eq,rule_format])
-    unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
-    by simp (simp add: field_simps norm_minus_commute)
+  have "z \<in> interior (ball c d)"
+    using y \<open>0 < e\<close> \<open>e \<le> 1\<close>
+    apply (simp add: interior_open[OF open_ball] z_def dist_norm)
+    by (simp add: field_simps norm_minus_commute)
+  then have "z \<in> interior S"
+    using d interiorI interior_ball by blast
   then show ?thesis
     unfolding *
     using mem_interior_convex_shrink \<open>y \<in> S\<close> assms by blast
@@ -216,10 +207,8 @@
           show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
             using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
           show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<in> interior S"
-            apply (clarsimp simp add: min_def a)
-            apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
-            using \<open>0 < e\<close> False apply (auto simp: field_split_simps)
-            done
+            using \<open>0 < e\<close> False
+            by (auto simp add: min_def a intro: mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
         qed
       qed
     qed
@@ -395,23 +384,22 @@
          (simp_all add: sum.If_cases i) }
   note ** = this
   show ?thesis
-    apply (rule that[of ?a])
-    unfolding interior_std_simplex mem_Collect_eq
-  proof safe
-    fix i :: 'a
-    assume i: "i \<in> Basis"
-    show "0 < ?a \<bullet> i"
-      unfolding **[OF i] by (auto simp add: Suc_le_eq)
-  next
-    have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D"
-      apply (rule sum.cong)
-      apply rule
-      apply auto
-      done
-    also have "\<dots> < 1"
-      unfolding sum_constant divide_inverse[symmetric]
-      by (auto simp add: field_simps)
-    finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
+  proof
+    show "?a \<in> interior(convex hull (insert 0 Basis))"
+      unfolding interior_std_simplex mem_Collect_eq
+    proof safe
+      fix i :: 'a
+      assume i: "i \<in> Basis"
+      show "0 < ?a \<bullet> i"
+        unfolding **[OF i] by (auto simp add: Suc_le_eq)
+    next
+      have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D"
+        by (auto intro: sum.cong)
+      also have "\<dots> < 1"
+        unfolding sum_constant divide_inverse[symmetric]
+        by (auto simp add: field_simps)
+      finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
+    qed
   qed
 qed
 
@@ -451,11 +439,8 @@
         fix i :: 'a
         assume "i \<in> D"
         then have "\<forall>j\<in>D. 0 \<le> (x - (e / 2) *\<^sub>R i) \<bullet> j"
-          apply -
-          apply (rule as[THEN conjunct1])
           using D \<open>e > 0\<close> x0
-          apply (auto simp: dist_norm inner_simps inner_Basis)
-          done
+          by (force simp: dist_norm inner_simps inner_Basis intro!: as[THEN conjunct1])
         then show "0 < x \<bullet> i"
           using \<open>e > 0\<close> \<open>i \<in> D\<close> D  by (force simp: inner_simps inner_Basis)
       next
@@ -506,10 +491,8 @@
       moreover have "?d > 0" using as using \<open>0 < card D\<close> by auto
       ultimately have h3: "min (Min (((\<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)
+      have "\<exists>e>0. ball x e \<inter> {x. \<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x \<bullet> i = 0}
+          \<subseteq> convex hull insert 0 D"
         unfolding substd_simplex[OF assms]
         apply (rule_tac x="min (Min (((\<bullet>) x) ` D)) ?d" in exI)
         apply (rule, rule h3)
@@ -549,8 +532,10 @@
           then show "0 \<le> y\<bullet>i"
             using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format]
             by (auto simp: inner_simps)
-        qed (insert y2, auto)
+        qed (use y2 in auto)
       qed
+      then have "x \<in> rel_interior (convex hull (insert 0 ?p))"
+        using h0 h2 rel_interior_ball by force
     }
     ultimately have
       "\<And>x. x \<in> rel_interior (convex hull insert 0 D) \<longleftrightarrow>
@@ -569,64 +554,61 @@
   let ?D = D
   let ?a = "sum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card D)) *\<^sub>R b) ?D"
   have "finite D"
-    apply (rule finite_subset)
-    using assms(2)
-    apply auto
-    done
+    using assms finite_Basis infinite_super by blast
   then have d1: "0 < real (card D)"
     using \<open>D \<noteq> {}\<close> by auto
   {
     fix i
     assume "i \<in> D"
-    have "?a \<bullet> i = inverse (2 * real (card D))"
-      apply (rule trans[of _ "sum (\<lambda>j. if i = j then inverse (2 * real (card D)) else 0) ?D"])
+    have "?a \<bullet> i = sum (\<lambda>j. if i = j then inverse (2 * real (card D)) else 0) ?D"
       unfolding inner_sum_left
-      apply (rule sum.cong)
-      using \<open>i \<in> D\<close> \<open>finite D\<close> sum.delta'[of D i "(\<lambda>k. inverse (2 * real (card D)))"]
-        d1 assms(2)
-      by (auto simp: inner_Basis rev_subsetD[OF _ assms(2)])
+      using \<open>i \<in> D\<close> by (auto simp: inner_Basis subsetD[OF assms(2)] intro: sum.cong)
+    also have "... = inverse (2 * real (card D))"
+      using \<open>i \<in> D\<close> \<open>finite D\<close> by auto
+    finally have "?a \<bullet> i = inverse (2 * real (card D))" .
   }
   note ** = this
   show ?thesis
-    apply (rule that[of ?a])
-    unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
-  proof safe
-    fix i
-    assume "i \<in> D"
-    have "0 < inverse (2 * real (card D))"
-      using d1 by auto
-    also have "\<dots> = ?a \<bullet> i" using **[of i] \<open>i \<in> D\<close>
-      by auto
-    finally show "0 < ?a \<bullet> i" by auto
-  next
-    have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real (card D))) ?D"
-      by (rule sum.cong) (rule refl, rule **)
-    also have "\<dots> < 1"
-      unfolding sum_constant divide_real_def[symmetric]
-      by (auto simp add: field_simps)
-    finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
-  next
-    fix i
-    assume "i \<in> Basis" and "i \<notin> D"
-    have "?a \<in> span D"
-    proof (rule span_sum[of D "(\<lambda>b. b /\<^sub>R (2 * real (card D)))" D])
-      {
-        fix x :: "'a::euclidean_space"
-        assume "x \<in> D"
-        then have "x \<in> span D"
-          using span_base[of _ "D"] by auto
-        then have "x /\<^sub>R (2 * real (card D)) \<in> span D"
-          using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto
-      }
-      then show "\<And>x. x\<in>D \<Longrightarrow> x /\<^sub>R (2 * real (card D)) \<in> span D"
+  proof
+    show "?a \<in> rel_interior (convex hull (insert 0 D))"
+      unfolding rel_interior_substd_simplex[OF assms(2)] 
+    proof safe
+      fix i
+      assume "i \<in> D"
+      have "0 < inverse (2 * real (card D))"
+        using d1 by auto
+      also have "\<dots> = ?a \<bullet> i" using **[of i] \<open>i \<in> D\<close>
         by auto
+      finally show "0 < ?a \<bullet> i" by auto
+    next
+      have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real (card D))) ?D"
+        by (rule sum.cong) (rule refl, rule **)
+      also have "\<dots> < 1"
+        unfolding sum_constant divide_real_def[symmetric]
+        by (auto simp add: field_simps)
+      finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
+    next
+      fix i
+      assume "i \<in> Basis" and "i \<notin> D"
+      have "?a \<in> span D"
+      proof (rule span_sum[of D "(\<lambda>b. b /\<^sub>R (2 * real (card D)))" D])
+        {
+          fix x :: "'a::euclidean_space"
+          assume "x \<in> D"
+          then have "x \<in> span D"
+            using span_base[of _ "D"] by auto
+          then have "x /\<^sub>R (2 * real (card D)) \<in> span D"
+            using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto
+        }
+        then show "\<And>x. x\<in>D \<Longrightarrow> x /\<^sub>R (2 * real (card D)) \<in> span D"
+          by auto
+      qed
+      then show "?a \<bullet> i = 0 "
+        using \<open>i \<notin> D\<close> unfolding span_substd_basis[OF assms(2)] using \<open>i \<in> Basis\<close> by auto
     qed
-    then show "?a \<bullet> i = 0 "
-      using \<open>i \<notin> D\<close> unfolding span_substd_basis[OF assms(2)] using \<open>i \<in> Basis\<close> by auto
   qed
 qed
 
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Relative interior of convex set\<close>
 
 lemma rel_interior_convex_nonempty_aux:
diff -r b7d6b9e71f88 -r a6cbf8ce979e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Aug 25 23:21:38 2020 +0200
+++ b/src/HOL/Transcendental.thy	Wed Aug 26 15:59:21 2020 +0100
@@ -1421,30 +1421,27 @@
   have S_comm: "\<And>n. S x n * y = y * S x n"
     by (simp add: power_commuting_commutes comm S_def)
 
-  have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
-    by (simp only: times_S)
-  also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n - i))"
-    by (simp only: Suc)
+  have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * (\<Sum>i\<le>n. S x i * S y (n - i))"
+    by (metis Suc.hyps times_S)
   also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n - i)) + y * (\<Sum>i\<le>n. S x i * S y (n - i))"
     by (rule distrib_right)
   also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n - i)) + (\<Sum>i\<le>n. S x i * y * S y (n - i))"
     by (simp add: sum_distrib_left ac_simps S_comm)
   also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n - i)) + (\<Sum>i\<le>n. S x i * (y * S y (n - i)))"
     by (simp add: ac_simps)
-  also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n - i))) +
-      (\<Sum>i\<le>n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))"
+  also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n - i))) 
+                + (\<Sum>i\<le>n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))"
     by (simp add: times_S Suc_diff_le)
-  also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n - i))) =
-      (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n - i)))"
+  also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n - i)))
+           = (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n - i)))"
     by (subst sum.atMost_Suc_shift) simp
-  also have "(\<Sum>i\<le>n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i))) =
-      (\<Sum>i\<le>Suc n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))"
+  also have "(\<Sum>i\<le>n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))
+           = (\<Sum>i\<le>Suc n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))"
     by simp
-  also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n - i))) +
-        (\<Sum>i\<le>Suc n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i))) =
-      (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n - i)))"
-    by (simp only: sum.distrib [symmetric] scaleR_left_distrib [symmetric]
-        of_nat_add [symmetric]) simp
+  also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n - i)))
+           + (\<Sum>i\<le>Suc n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i))) 
+           = (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n - i)))"
+    by (simp flip: sum.distrib scaleR_add_left of_nat_add) 
   also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
     by (simp only: scaleR_right.sum)
   finally show "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"