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`