src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 56541 0e3abadbef39 parent 56371 fb9ae0727548 child 56544 b60d5d119489
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Apr 11 17:53:16 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Apr 11 22:53:33 2014 +0200
1.3 @@ -854,7 +854,7 @@
1.4  proof -
1.5    def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
1.6    then have e: "e' > 0"
1.7 -    using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
1.8 +    using assms by (auto simp: DIM_positive)
1.9    have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
1.10    proof
1.11      fix i
1.12 @@ -2538,7 +2538,7 @@
1.13      apply (simp only: dist_norm [symmetric])
1.14      apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
1.15      apply (rule mult_strict_right_mono)
1.16 -    apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \<noteq> y`)
1.17 +    apply (simp add: k_def zero_less_dist_iff `0 < r` `x \<noteq> y`)
1.18      apply (simp add: zero_less_dist_iff `x \<noteq> y`)
1.19      done
1.20    then have "z \<in> ball x (dist x y)"
1.21 @@ -2620,9 +2620,8 @@
1.22        then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
1.23          using d as(1)[unfolded subset_eq] by blast
1.24        have "y - x \<noteq> 0" using `x \<noteq> y` by auto
1.25 -      then have **:"d / (2 * norm (y - x)) > 0"
1.26 -        unfolding zero_less_norm_iff[symmetric]
1.27 -        using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
1.28 +      hence **:"d / (2 * norm (y - x)) > 0"
1.29 +        unfolding zero_less_norm_iff[symmetric] using `d>0` by auto
1.30        have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
1.31          norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
1.32          by (auto simp add: dist_norm algebra_simps)
1.33 @@ -4012,8 +4011,7 @@
1.34    {
1.35      fix e::real
1.36      assume "e > 0"
1.37 -    then have "e / real_of_nat DIM('a) > 0"
1.38 -      by (auto intro!: divide_pos_pos DIM_positive)
1.39 +    hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
1.40      with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
1.41        by simp
1.42      moreover
1.43 @@ -4142,7 +4140,7 @@
1.44    have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
1.45      by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
1.46    also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
1.47 -    by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
1.48 +    by (rule divide_left_mono) (auto simp: `0 < e`)
1.49    also have "\<dots> = e" by simp
1.50    finally show  "\<exists>n. 1 / real (Suc n) < e" ..
1.51  qed
1.52 @@ -7141,8 +7139,7 @@
1.53      using `norm b >0`
1.54      unfolding zero_less_norm_iff
1.55      by auto
1.56 -  ultimately have "0 < norm (f b) / norm b"
1.57 -    by (simp only: divide_pos_pos)
1.58 +  ultimately have "0 < norm (f b) / norm b" by simp
1.59    moreover
1.60    {
1.61      fix x
1.62 @@ -7155,8 +7152,7 @@
1.63        case False
1.64        then have *: "0 < norm a / norm x"
1.65          using `a\<noteq>0`
1.66 -        unfolding zero_less_norm_iff[symmetric]
1.67 -        by (simp only: divide_pos_pos)
1.68 +        unfolding zero_less_norm_iff[symmetric] by simp
1.69        have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s"
1.70          using s[unfolded subspace_def] by auto
1.71        then have "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}"
1.72 @@ -7403,10 +7399,8 @@
1.73        case False
1.74        then have "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
1.75          by (metis False d_def less_le)
1.76 -      then have "0 < e * (1 - c) / d"
1.77 -        using `e>0` and `1-c>0`
1.78 -        using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"]
1.79 -        by auto
1.80 +      hence "0 < e * (1 - c) / d"
1.81 +        using `e>0` and `1-c>0` mult_pos_pos[of e "1 - c"] by auto
1.82        then obtain N where N:"c ^ N < e * (1 - c) / d"
1.83          using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
1.84        {
1.85 @@ -7416,11 +7410,8 @@
1.86            using power_decreasing[OF `n\<ge>N`, of c] by auto
1.87          have "1 - c ^ (m - n) > 0"
1.88            using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
1.89 -        then have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
1.90 -          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"]
1.91 -          using divide_pos_pos[of "d * (1 - c ^ (m - n))" "1 - c"]
1.92 -          using `0 < 1 - c`
1.93 -          by auto
1.94 +        hence **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
1.95 +          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"] `0 < 1 - c` by auto
1.96
1.97          have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
1.98            using cf_z2[of n "m - n"] and `m>n`
```