src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 56479 91958d4b30f7
parent 56409 36489d77c484
child 56480 093ea91498e6
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -2277,7 +2277,9 @@
     1.4        using Min_ge_iff[of i 0 ] and obt(1)
     1.5        unfolding t_def i_def
     1.6        using obt(4)[unfolded le_less]
     1.7 -      apply (auto simp: divide_le_0_iff divide_minus_right)
     1.8 +      apply auto
     1.9 +      unfolding divide_le_0_iff
    1.10 +      apply auto
    1.11        done
    1.12      have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
    1.13      proof
    1.14 @@ -2314,7 +2316,7 @@
    1.15  
    1.16      obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
    1.17        using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
    1.18 -    then have a: "a \<in> s" "u a + t * w a = 0" by (auto simp: divide_minus_right)
    1.19 +    then have a: "a \<in> s" "u a + t * w a = 0" by auto
    1.20      have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
    1.21        unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto
    1.22      have "(\<Sum>v\<in>s. u v + t * w v) = 1"