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`