# HG changeset patch # User nipkow # Date 1575059358 -3600 # Node ID 6c208c2dca532644e2eef82de7788df027da2146 # Parent a1e94be66bd6c16a86fc9602522e73b2f9ef0e63 tuned diff -r a1e94be66bd6 -r 6c208c2dca53 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 \D \ {}\ \finite D\ by (simp add: card_gt_0_iff) have "Min (((\) x) ` D) > 0" - using as \D \ {}\ \finite D\ by (simp add: Min_gr_iff) + using as \D \ {}\ \finite D\ by (simp) moreover have "?d > 0" using as using \0 < card D\ by auto ultimately have h3: "min (Min (((\) x) ` D)) ?d > 0" by auto @@ -957,8 +957,7 @@ then have "rel_interior S \ {}" 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 \ {}" - using assms rel_interior_empty by auto + using assms by auto have nonemp: "f -` S \ {}" by (metis assms(3) rel_interior_subset subset_empty vimage_mono) then have "S \ (range f) \ {}" @@ -2179,7 +2177,7 @@ then have "\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 (\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 \ S \ (\c. c > 0 \ (*\<^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 \ 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 (\(S ` I))" @@ -3375,7 +3373,7 @@ } note * = this have "y \ 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 \ 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 \ x \ r}) = DIM('a)" if "(a = 0 \ r \ 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 \ x = 0} \ 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 \ 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 \ closed_segment a c" moreover have "\ 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: \\ affine_dependent c\ \b \ c\ aff_dim_affine_independent aff_dim_UNIV card_Diff_subset of_nat_diff) + by (simp add: \\ affine_dependent c\ \b \ c\ 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 \ B}" by (simp add: affine_independent_card_dim_diffs [OF ind \c \ B\]) also have "... = dim {x - c | x. x \ affine hull B}" - by (simp add: diffs_affine_hull_span \c \ B\ dim_span) + by (simp add: diffs_affine_hull_span \c \ B\) also have "... = dim {x - a |x. x \ S}" by (simp add: affS aff *) finally show ?thesis .