src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 57512 cc97b347b301
parent 57448 159e45728ceb
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -2725,7 +2725,7 @@
     1.4  
     1.5  lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
     1.6    unfolding bounded_def
     1.7 -  by auto (metis add_commute add_le_cancel_right dist_commute dist_triangle_le)
     1.8 +  by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)
     1.9  
    1.10  lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
    1.11    unfolding bounded_any_center [where a=0]
    1.12 @@ -2859,7 +2859,7 @@
    1.13    then show ?thesis
    1.14      unfolding bounded_pos
    1.15      apply (rule_tac x="b*B" in exI)
    1.16 -    using b B by (auto simp add: mult_commute)
    1.17 +    using b B by (auto simp add: mult.commute)
    1.18  qed
    1.19  
    1.20  lemma bounded_scaling:
    1.21 @@ -2901,7 +2901,7 @@
    1.22  
    1.23  lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"
    1.24    by (auto simp: bounded_def bdd_below_def dist_real_def)
    1.25 -     (metis abs_le_D1 add_commute diff_le_eq)
    1.26 +     (metis abs_le_D1 add.commute diff_le_eq)
    1.27  
    1.28  (* TODO: remove the following lemmas about Inf and Sup, is now in conditionally complete lattice *)
    1.29  
    1.30 @@ -6801,7 +6801,7 @@
    1.31      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
    1.32        unfolding image_iff Bex_def mem_box
    1.33        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
    1.34 -      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
    1.35 +      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult.commute diff_le_iff inner_distrib inner_diff_left)
    1.36        done
    1.37    }
    1.38    moreover
    1.39 @@ -6811,7 +6811,7 @@
    1.40      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
    1.41        unfolding image_iff Bex_def mem_box
    1.42        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
    1.43 -      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
    1.44 +      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult.commute diff_le_iff inner_distrib inner_diff_left)
    1.45        done
    1.46    }
    1.47    ultimately show ?thesis using False by (auto simp: cbox_def)
    1.48 @@ -7175,7 +7175,7 @@
    1.49        then show "norm (f b) / norm b * norm x \<le> norm (f x)"
    1.50          using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
    1.51          unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
    1.52 -        by (auto simp add: mult_commute pos_le_divide_eq pos_divide_le_eq)
    1.53 +        by (auto simp add: mult.commute pos_le_divide_eq pos_divide_le_eq)
    1.54      qed
    1.55    }
    1.56    ultimately show ?thesis by auto
    1.57 @@ -7406,7 +7406,7 @@
    1.58      proof (cases "d = 0")
    1.59        case True
    1.60        have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0`
    1.61 -        by (metis mult_zero_left mult_commute real_mult_le_cancel_iff1)
    1.62 +        by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1)
    1.63        from True have "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def
    1.64          by (simp add: *)
    1.65        then show ?thesis using `e>0` by auto
    1.66 @@ -7431,12 +7431,12 @@
    1.67          have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
    1.68            using cf_z2[of n "m - n"] and `m>n`
    1.69            unfolding pos_le_divide_eq[OF `1-c>0`]
    1.70 -          by (auto simp add: mult_commute dist_commute)
    1.71 +          by (auto simp add: mult.commute dist_commute)
    1.72          also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
    1.73            using mult_right_mono[OF * order_less_imp_le[OF **]]
    1.74 -          unfolding mult_assoc by auto
    1.75 +          unfolding mult.assoc by auto
    1.76          also have "\<dots> < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
    1.77 -          using mult_strict_right_mono[OF N **] unfolding mult_assoc by auto
    1.78 +          using mult_strict_right_mono[OF N **] unfolding mult.assoc by auto
    1.79          also have "\<dots> = e * (1 - c ^ (m - n))"
    1.80            using c and `d>0` and `1 - c > 0` by auto
    1.81          also have "\<dots> \<le> e" using c and `1 - c ^ (m - n) > 0` and `e>0`