src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 58776 95e58e04e534
parent 57865 dcfb33c26f50
child 58877 262572d90bc6
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -5915,29 +5915,10 @@
     1.4    proof -
     1.5      fix y
     1.6      assume as: "y\<in>cbox (x - ?d) (x + ?d)"
     1.7 -    {
     1.8 -      fix i :: 'a
     1.9 -      assume i: "i \<in> Basis"
    1.10 -      have "x \<bullet> i \<le> d + y \<bullet> i" "y \<bullet> i \<le> d + x \<bullet> i"
    1.11 -        using as[unfolded mem_box, THEN bspec[where x=i]] i
    1.12 -        by (auto simp: inner_simps)
    1.13 -      then have "1 \<ge> inverse d * (x \<bullet> i - y \<bullet> i)" "1 \<ge> inverse d * (y \<bullet> i - x \<bullet> i)"
    1.14 -        apply (rule_tac[!] mult_left_le_imp_le[OF _ assms])
    1.15 -        unfolding mult.assoc[symmetric]
    1.16 -        using assms
    1.17 -        by (auto simp add: field_simps)
    1.18 -      then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
    1.19 -        "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
    1.20 -        using `0<d` by (auto simp add: field_simps) }
    1.21      then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
    1.22 -      unfolding mem_box using assms
    1.23 -      by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
    1.24 -    then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
    1.25 -      apply -
    1.26 -      apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
    1.27 -      using assms
    1.28 -      apply auto
    1.29 -      done
    1.30 +      using assms by (simp add: mem_box field_simps inner_simps)
    1.31 +    with `0 < d` show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
    1.32 +      by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
    1.33    next
    1.34      fix y z
    1.35      assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
    1.36 @@ -6076,7 +6057,7 @@
    1.37            using `0 < t` `2 < t` and `y \<in> s` `w \<in> s`
    1.38            by (auto simp add:field_simps)
    1.39          also have "\<dots> = (f w + t * f y) / (1 + t)"
    1.40 -          using `t > 0` unfolding divide_inverse by (auto simp add: field_simps)
    1.41 +          using `t > 0` by (auto simp add: divide_simps)
    1.42          also have "\<dots> < e + f y"
    1.43            using `t > 0` * `e > 0` by (auto simp add: field_simps)
    1.44          finally have "f x - f y < e" by auto