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.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.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`
```