tuned
authornipkow
Fri, 29 Nov 2019 21:29:18 +0100
changeset 71376 6c208c2dca53
parent 71375 a1e94be66bd6
child 71380 65192ac7eaf2
tuned
src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Fri Nov 29 17:43:00 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Nov 29 21:29:18 2019 +0100
@@ -745,7 +745,7 @@
       have "0 < card D" using \<open>D \<noteq> {}\<close> \<open>finite D\<close>
         by (simp add: card_gt_0_iff)
       have "Min (((\<bullet>) x) ` D) > 0"
-        using as \<open>D \<noteq> {}\<close> \<open>finite D\<close> by (simp add: Min_gr_iff)
+        using as \<open>D \<noteq> {}\<close> \<open>finite D\<close> by (simp)
       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
@@ -957,8 +957,7 @@
     then have "rel_interior S \<noteq> {}"
       using rel_interior_translation [of "- a"] by simp
   }
-  then show ?thesis
-    using rel_interior_empty by auto
+  then show ?thesis by auto
 qed
 
 lemma interior_simplex_nonempty:
@@ -1052,8 +1051,7 @@
     then show ?thesis using h1 by auto
   next
     case True
-    then have "rel_interior S = {}"
-      using rel_interior_empty by auto
+    then have "rel_interior S = {}" by auto
     then have "closure (rel_interior S) = {}"
       using closure_empty by auto
     with True show ?thesis by auto
@@ -1581,7 +1579,7 @@
     then have "affine hull S = UNIV"
       by auto
     then have "aff_dim S = int DIM('n)"
-      using aff_dim_affine_hull[of S] by (simp add: aff_dim_UNIV)
+      using aff_dim_affine_hull[of S] by (simp)
     then have False
       using False by auto
   }
@@ -1984,7 +1982,7 @@
 proof (cases "S = {}")
   case True
   then show ?thesis
-    using assms rel_interior_empty rel_interior_eq_empty by auto
+    using assms by auto
 next
   case False
   interpret linear f by fact
@@ -2043,7 +2041,7 @@
 proof -
   interpret linear f by fact
   have "S \<noteq> {}"
-    using assms rel_interior_empty by auto
+    using assms by auto
   have nonemp: "f -` S \<noteq> {}"
     by (metis assms(3) rel_interior_subset subset_empty vimage_mono)
   then have "S \<inter> (range f) \<noteq> {}"
@@ -2179,7 +2177,7 @@
   then have "\<Inter>I = {}"
     using assms unfolding rel_open_def by auto
   then show ?thesis
-    unfolding rel_open_def using rel_interior_empty by auto
+    unfolding rel_open_def by auto
 next
   case False
   then have "rel_open (\<Inter>I)"
@@ -2209,7 +2207,7 @@
   then have "f -` S = {}"
     using assms unfolding rel_open_def by auto
   then show ?thesis
-    unfolding rel_open_def using rel_interior_empty by auto
+    unfolding rel_open_def by auto
 next
   case False
   then have "rel_open (f -` S)"
@@ -2333,7 +2331,7 @@
 proof (cases "S = {}")
   case True
   then show ?thesis
-    by (simp add: rel_interior_empty cone_0)
+    by (simp add: cone_0)
 next
   case False
   then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
@@ -2353,7 +2351,7 @@
 proof (cases "S = {}")
   case True
   then show ?thesis
-    by (simp add: rel_interior_empty cone_hull_empty)
+    by (simp add: cone_hull_empty)
 next
   case False
   then obtain s where "s \<in> S" by auto
@@ -2980,7 +2978,7 @@
 proof (cases "I = {}")
   case True
   then show ?thesis
-    using convex_hull_empty rel_interior_empty by auto
+    using convex_hull_empty by auto
 next
   case False
   define C0 where "C0 = convex hull (\<Union>(S ` I))"
@@ -3375,7 +3373,7 @@
       } note * = this
       have "y \<notin> rel_interior (convex hull s)"
         using y
-        apply (simp add: mem_rel_interior affine_hull_convex_hull)
+        apply (simp add: mem_rel_interior)
         apply (auto simp: convex_hull_finite [OF fs])
         apply (drule_tac x=u in spec)
         apply (auto intro: *)
@@ -4081,7 +4079,7 @@
   case False with assms show ?thesis
     apply (auto simp: collinear_3 collinear_lemma between_norm)
     apply (drule_tac x="-(norm(b - x) / norm(x - a))" in spec)
-    apply (simp add: vector_add_divide_simps eq_vector_fraction_iff real_vector.scale_minus_right [symmetric])
+    apply (simp add: vector_add_divide_simps real_vector.scale_minus_right [symmetric])
     done
 qed
 
@@ -4925,11 +4923,11 @@
         (if a = 0 \<and> r < 0 then -1 else DIM('a))"
 proof -
   have "int (DIM('a)) = aff_dim (UNIV::'a set)"
-    by (simp add: aff_dim_UNIV)
+    by (simp)
   then have "aff_dim (affine hull {x. a \<bullet> x \<le> r}) = DIM('a)" if "(a = 0 \<longrightarrow> r \<ge> 0)"
     using that by (simp add: affine_hull_halfspace_le not_less)
   then show ?thesis
-    by (force simp: aff_dim_affine_hull)
+    by (force)
 qed
 
 lemma aff_dim_halfspace_gt:
@@ -5105,11 +5103,11 @@
   then have "aff_dim {x. a \<bullet> x = 0} \<le> 0"
     by (simp add: affine_bounded_eq_lowdim affine_hyperplane)
   with assms show "DIM('a) = 1"
-    by (simp add: le_Suc_eq aff_dim_hyperplane)
+    by (simp add: le_Suc_eq)
 next
   assume "DIM('a) = 1"
   then show "bounded {x. a \<bullet> x = 0}"
-    by (simp add: aff_dim_hyperplane affine_bounded_eq_lowdim affine_hyperplane assms)
+    by (simp add: affine_bounded_eq_lowdim affine_hyperplane assms)
 qed
 
 lemma bounded_hyperplane_eq_trivial:
@@ -5573,7 +5571,7 @@
   proof
     assume "b \<in> closed_segment a c"
     moreover have "\<not> affine_dependent {a, c}"
-      by (simp add: affine_independent_2)
+      by (simp)
     ultimately show ?thesis
       using False convex_hull_exchange_Int [of "{a,c}" b "{a}" "{c}"]
       by (simp add: segment_convex_hull insert_commute)
@@ -5631,7 +5629,7 @@
       by (simp add: aff_dim_affine_independent indb)
     then show ?thesis
       using fbc aff
-      by (simp add: \<open>\<not> affine_dependent c\<close> \<open>b \<subseteq> c\<close> aff_dim_affine_independent aff_dim_UNIV card_Diff_subset of_nat_diff)
+      by (simp add: \<open>\<not> affine_dependent c\<close> \<open>b \<subseteq> c\<close> aff_dim_affine_independent card_Diff_subset of_nat_diff)
   qed
   show ?thesis
   proof (cases "c = b")
@@ -6099,7 +6097,7 @@
   also have "... = dim {x - c |x. x \<in> B}"
     by (simp add: affine_independent_card_dim_diffs [OF ind \<open>c \<in> B\<close>])
   also have "... = dim {x - c | x. x \<in> affine hull B}"
-     by (simp add: diffs_affine_hull_span \<open>c \<in> B\<close> dim_span)
+     by (simp add: diffs_affine_hull_span \<open>c \<in> B\<close>)
   also have "... = dim {x - a |x. x \<in> S}"
      by (simp add: affS aff *)
    finally show ?thesis .