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`