src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 56544 b60d5d119489 parent 56541 0e3abadbef39 child 56742 678a52e676b6
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Apr 11 23:22:00 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 12 17:26:27 2014 +0200
1.3 @@ -2832,9 +2832,7 @@
1.4    then show ?thesis
1.5      unfolding bounded_pos
1.6      apply (rule_tac x="b*B" in exI)
1.7 -    using b B mult_pos_pos [of b B]
1.8 -    apply (auto simp add: mult_commute)
1.9 -    done
1.10 +    using b B by (auto simp add: mult_commute)
1.11  qed
1.12
1.13  lemma bounded_scaling:
1.14 @@ -4138,7 +4136,7 @@
1.15    obtains n :: nat where "1 / (Suc n) < e"
1.16  proof atomize_elim
1.17    have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
1.18 -    by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
1.19 +    by (rule divide_strict_left_mono) (auto simp: `0 < e`)
1.20    also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
1.21      by (rule divide_left_mono) (auto simp: `0 < e`)
1.22    also have "\<dots> = e" by simp
1.23 @@ -5321,9 +5319,7 @@
1.24        and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
1.25        by auto
1.26      have "e * abs c > 0"
1.27 -      using assms(1)[unfolded zero_less_abs_iff[symmetric]]
1.28 -      using mult_pos_pos[OF `e>0`]
1.29 -      by auto
1.30 +      using assms(1)[unfolded zero_less_abs_iff[symmetric]] `e>0` by auto
1.31      moreover
1.32      {
1.33        fix y
1.34 @@ -7036,8 +7032,7 @@
1.35      fix d :: real
1.36      assume "d > 0"
1.37      then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
1.38 -      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]]
1.39 -        and e and mult_pos_pos[of e d]
1.40 +      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] e
1.41        by auto
1.42      {
1.43        fix n
1.44 @@ -7400,7 +7395,7 @@
1.45        then have "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
1.46          by (metis False d_def less_le)
1.47        hence "0 < e * (1 - c) / d"
1.48 -        using `e>0` and `1-c>0` mult_pos_pos[of e "1 - c"] by auto
1.49 +        using `e>0` and `1-c>0` by auto
1.50        then obtain N where N:"c ^ N < e * (1 - c) / d"
1.51          using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
1.52        {
1.53 @@ -7411,7 +7406,7 @@
1.54          have "1 - c ^ (m - n) > 0"
1.55            using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
1.56          hence **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
1.57 -          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"] `0 < 1 - c` by auto
1.58 +          using `d>0` `0 < 1 - c` by auto
1.59
1.60          have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
1.61            using cf_z2[of n "m - n"] and `m>n`
```