src/HOL/Analysis/Polytope.thy
changeset 68072 493b818e8e10
parent 67968 a5ad4c015d1c
child 68073 fad29d2a17a5
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Wed Apr 18 21:12:50 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Wed May 02 13:49:38 2018 +0200
     1.3 @@ -197,8 +197,7 @@
     1.4        by (simp add: algebra_simps d_def) (simp add: divide_simps)
     1.5      have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))"
     1.6        using False nbc
     1.7 -      apply (simp add: algebra_simps divide_simps)
     1.8 -      by (metis mult_eq_0_iff norm_eq_zero norm_imp_pos_and_ge norm_pths(2) real_scaleR_def scaleR_left.add zero_less_norm_iff)
     1.9 +      by (simp add: divide_simps) (simp add: algebra_simps)
    1.10      have "b \<in> open_segment d c"
    1.11        apply (simp add: open_segment_image_interval)
    1.12        apply (simp add: d_def algebra_simps image_def)
    1.13 @@ -2673,7 +2672,8 @@
    1.14  lemma polyhedron_negations:
    1.15    fixes S :: "'a :: euclidean_space set"
    1.16    shows   "polyhedron S \<Longrightarrow> polyhedron(image uminus S)"
    1.17 -by (auto simp: polyhedron_linear_image_eq linear_uminus bij_uminus)
    1.18 +  by (subst polyhedron_linear_image_eq)
    1.19 +    (auto simp: bij_uminus intro!: linear_uminus)
    1.20  
    1.21  subsection\<open>Relation between polytopes and polyhedra\<close>
    1.22