remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

--- a/NEWS	Thu Aug 18 17:42:35 2011 +0200
+++ b/NEWS	Thu Aug 18 13:36:58 2011 -0700
@@ -199,6 +199,19 @@
   tendsto_vector   ~> vec_tendstoI
   Cauchy_vector    ~> vec_CauchyI
 
+* Complex_Main: The locale interpretations for the bounded_linear and
+bounded_bilinear locales have been removed, in order to reduce the
+number of duplicate lemmas. Users must use the original names for
+distributivity theorems, potential INCOMPATIBILITY.
+
+  divide.add ~> add_divide_distrib
+  divide.diff ~> diff_divide_distrib
+  divide.setsum ~> setsum_divide_distrib
+  mult.add_right ~> right_distrib
+  mult.diff_right ~> right_diff_distrib
+  mult_right.setsum ~> setsum_right_distrib
+  mult_left.diff ~> left_diff_distrib
+
 
 *** Document preparation ***
 

--- a/src/HOL/Import/HOLLightReal.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Import/HOLLightReal.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -112,7 +112,7 @@
 
 lemma REAL_DIFFSQ:
   "((x :: real) + y) * (x - y) = x * x - y * y"
-  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
+  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
 
 lemma REAL_ABS_TRIANGLE_LE:
   "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
@@ -295,7 +295,7 @@
    (\<forall>(x :: real). 0 * x = 0) \<and>
    (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
    (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
-  by (auto simp add: mult.add_right)
+  by (auto simp add: right_distrib)
 
 lemma REAL_COMPLETE:
   "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>

--- a/src/HOL/Library/Convex.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Library/Convex.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -129,7 +129,7 @@
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
-    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     from this asms
     have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
     hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
@@ -410,7 +410,7 @@
     have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
     hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
-    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
+    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     have "convex C" using asms by auto
     hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
       using asms convex_setsum[OF `finite s`
@@ -433,7 +433,7 @@
       using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
         OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
     also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
-      unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
+      unfolding setsum_right_distrib[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
     also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
     also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
     finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"

--- a/src/HOL/Library/FrechetDeriv.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -5,7 +5,7 @@
 header {* Frechet Derivative *}
 
 theory FrechetDeriv
-imports Lim Complex_Main
+imports Complex_Main
 begin
 
 definition
@@ -398,9 +398,11 @@
     by (simp only: FDERIV_lemma)
 qed
 
-lemmas FDERIV_mult = mult.FDERIV
+lemmas FDERIV_mult =
+  bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
 
-lemmas FDERIV_scaleR = scaleR.FDERIV
+lemmas FDERIV_scaleR =
+  bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
 
 
 subsection {* Powers *}
@@ -427,10 +429,10 @@
 subsection {* Inverse *}
 
 lemmas bounded_linear_mult_const =
-  mult.bounded_linear_left [THEN bounded_linear_compose]
+  bounded_linear_mult_left [THEN bounded_linear_compose]
 
 lemmas bounded_linear_const_mult =
-  mult.bounded_linear_right [THEN bounded_linear_compose]
+  bounded_linear_mult_right [THEN bounded_linear_compose]
 
 lemma FDERIV_inverse:
   fixes x :: "'a::real_normed_div_algebra"
@@ -510,7 +512,7 @@
   fixes x :: "'a::real_normed_field" shows
   "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
  apply (unfold fderiv_def)
- apply (simp add: mult.bounded_linear_left)
+ apply (simp add: bounded_linear_mult_left)
  apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
  apply (subst diff_divide_distrib)
  apply (subst times_divide_eq_left [symmetric])

--- a/src/HOL/Library/Inner_Product.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -5,7 +5,7 @@
 header {* Inner Product Spaces and the Gradient Derivative *}
 
 theory Inner_Product
-imports Complex_Main FrechetDeriv
+imports FrechetDeriv
 begin
 
 subsection {* Real inner product spaces *}
@@ -43,6 +43,9 @@
 lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
   by (simp add: diff_minus inner_add_left)
 
+lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
+  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
+
 text {* Transfer distributivity rules to right argument. *}
 
 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
@@ -60,6 +63,9 @@
 lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
   using inner_diff_left [of y z x] by (simp only: inner_commute)
 
+lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
+  using inner_setsum_left [of f A x] by (simp only: inner_commute)
+
 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
 lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
@@ -148,8 +154,8 @@
 setup {* Sign.add_const_constraint
   (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
 
-interpretation inner:
-  bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
+lemma bounded_bilinear_inner:
+  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
 proof
   fix x y z :: 'a and r :: real
   show "inner (x + y) z = inner x z + inner y z"
@@ -167,15 +173,20 @@
   qed
 qed
 
-interpretation inner_left:
-  bounded_linear "\<lambda>x::'a::real_inner. inner x y"
-  by (rule inner.bounded_linear_left)
+lemmas tendsto_inner [tendsto_intros] =
+  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
+
+lemmas isCont_inner [simp] =
+  bounded_bilinear.isCont [OF bounded_bilinear_inner]
 
-interpretation inner_right:
-  bounded_linear "\<lambda>y::'a::real_inner. inner x y"
-  by (rule inner.bounded_linear_right)
+lemmas FDERIV_inner =
+  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
 
-declare inner.isCont [simp]
+lemmas bounded_linear_inner_left =
+  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
+
+lemmas bounded_linear_inner_right =
+  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
 
 
 subsection {* Class instances *}
@@ -260,29 +271,29 @@
   by simp
 
 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
-  unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
+  unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
 
 lemma GDERIV_add:
     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
-  unfolding gderiv_def inner_right.add by (rule FDERIV_add)
+  unfolding gderiv_def inner_add_right by (rule FDERIV_add)
 
 lemma GDERIV_minus:
     "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
-  unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
+  unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
 
 lemma GDERIV_diff:
     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
-  unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
+  unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
 
 lemma GDERIV_scaleR:
     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
       :> (scaleR (f x) dg + scaleR df (g x))"
-  unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
+  unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
   apply (rule FDERIV_subst)
-  apply (erule (1) scaleR.FDERIV)
+  apply (erule (1) FDERIV_scaleR)
   apply (simp add: mult_ac)
   done
 
@@ -306,7 +317,7 @@
   assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
 proof -
   have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
-    by (intro inner.FDERIV FDERIV_ident)
+    by (intro FDERIV_inner FDERIV_ident)
   have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
     by (simp add: fun_eq_iff inner_commute)
   have "0 < inner x x" using `x \<noteq> 0` by simp

--- a/src/HOL/Library/Product_Vector.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -489,11 +489,11 @@
 
 subsection {* Pair operations are linear *}
 
-interpretation fst: bounded_linear fst
+lemma bounded_linear_fst: "bounded_linear fst"
   using fst_add fst_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 
-interpretation snd: bounded_linear snd
+lemma bounded_linear_snd: "bounded_linear snd"
   using snd_add snd_scaleR
   by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
 

--- a/src/HOL/Lim.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Lim.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -321,17 +321,23 @@
   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
   by (rule tendsto_right_zero)
 
-lemmas LIM_mult = mult.LIM
+lemmas LIM_mult =
+  bounded_bilinear.LIM [OF bounded_bilinear_mult]
 
-lemmas LIM_mult_zero = mult.LIM_prod_zero
+lemmas LIM_mult_zero =
+  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
 
-lemmas LIM_mult_left_zero = mult.LIM_left_zero
+lemmas LIM_mult_left_zero =
+  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
 
-lemmas LIM_mult_right_zero = mult.LIM_right_zero
+lemmas LIM_mult_right_zero =
+  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
 
-lemmas LIM_scaleR = scaleR.LIM
+lemmas LIM_scaleR =
+  bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
 
-lemmas LIM_of_real = of_real.LIM
+lemmas LIM_of_real =
+  bounded_linear.LIM [OF bounded_linear_of_real]
 
 lemma LIM_power:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -446,11 +452,11 @@
   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   unfolding isCont_def by (rule LIM)
 
-lemmas isCont_scaleR [simp] = scaleR.isCont
+lemmas isCont_scaleR [simp] =
+  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
 
-lemma isCont_of_real [simp]:
-  "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
-  by (rule of_real.isCont)
+lemmas isCont_of_real [simp] =
+  bounded_linear.isCont [OF bounded_linear_of_real]
 
 lemma isCont_power [simp]:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"

--- a/src/HOL/Limits.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Limits.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -510,9 +510,9 @@
   "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F"
   by (rule bounded_linear_right [THEN bounded_linear.Zfun])
 
-lemmas Zfun_mult = mult.Zfun
-lemmas Zfun_mult_right = mult.Zfun_right
-lemmas Zfun_mult_left = mult.Zfun_left
+lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
+lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
+lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
 
 
 subsection {* Limits *}
@@ -752,7 +752,7 @@
 
 subsubsection {* Linear operators and multiplication *}
 
-lemma (in bounded_linear) tendsto [tendsto_intros]:
+lemma (in bounded_linear) tendsto:
   "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
   by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
 
@@ -760,7 +760,7 @@
   "(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
   by (drule tendsto, simp only: zero)
 
-lemma (in bounded_bilinear) tendsto [tendsto_intros]:
+lemma (in bounded_bilinear) tendsto:
   "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) F"
   by (simp only: tendsto_Zfun_iff prod_diff_prod
                  Zfun_add Zfun Zfun_left Zfun_right)
@@ -779,7 +779,14 @@
   "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) F"
   by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
 
-lemmas tendsto_mult = mult.tendsto
+lemmas tendsto_of_real [tendsto_intros] =
+  bounded_linear.tendsto [OF bounded_linear_of_real]
+
+lemmas tendsto_scaleR [tendsto_intros] =
+  bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]
+
+lemmas tendsto_mult [tendsto_intros] =
+  bounded_bilinear.tendsto [OF bounded_bilinear_mult]
 
 lemma tendsto_power [tendsto_intros]:
   fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -897,7 +904,7 @@
   apply (erule (1) inverse_diff_inverse)
   apply (rule Zfun_minus)
   apply (rule Zfun_mult_left)
-  apply (rule mult.Bfun_prod_Zfun)
+  apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
   apply (erule (1) Bfun_inverse)
   apply (simp add: tendsto_Zfun_iff)
   done
@@ -921,7 +928,7 @@
   fixes a b :: "'a::real_normed_field"
   shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
     \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
-  by (simp add: mult.tendsto tendsto_inverse divide_inverse)
+  by (simp add: tendsto_mult tendsto_inverse divide_inverse)
 
 lemma tendsto_sgn [tendsto_intros]:
   fixes l :: "'a::real_normed_vector"

--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -1202,7 +1202,7 @@
       show "\<bar>(f z - z) $$ i\<bar> < d / real n" unfolding euclidean_simps proof(rule *)
         show "\<bar>f x $$ i - x $$ i\<bar> \<le> norm (f y -f x) + norm (y - x)" apply(rule lem1[rule_format]) using as i  by auto
         show "\<bar>f x $$ i - f z $$ i\<bar> \<le> norm (f x - f z)" "\<bar>x $$ i - z $$ i\<bar> \<le> norm (x - z)"
-          unfolding euclidean_component.diff[THEN sym] by(rule component_le_norm)+
+          unfolding euclidean_component_diff[THEN sym] by(rule component_le_norm)+
         have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm]
           unfolding norm_minus_commute by auto
         also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto
@@ -1234,7 +1234,7 @@
     assume as:"\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
     { assume "x i = p \<or> x i = 0" 
       have "(\<chi>\<chi> i. real (x (b' i)) / real p) \<in> {0::'a..\<chi>\<chi> i. 1}" unfolding mem_interval 
-        apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+        apply safe unfolding euclidean_lambda_beta euclidean_component_zero
       proof (simp_all only: if_P) fix j assume j':"j<DIM('a)"
         hence j:"b' j \<in> {1..n}" using b' unfolding n_def bij_betw_def by auto
         show "0 \<le> real (x (b' j)) / real p"
@@ -1262,11 +1262,11 @@
     have "\<forall>i<DIM('a). q (b' i) \<in> {0..<p}" using q(1) b'[unfolded bij_betw_def] by auto 
     hence "\<forall>i<DIM('a). q (b' i) \<in> {0..p}" apply-apply(rule,erule_tac x=i in allE) by auto
     hence "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta
-      unfolding euclidean_component.zero apply (simp_all only: if_P)
+      unfolding euclidean_component_zero apply (simp_all only: if_P)
       apply(rule divide_nonneg_pos) using `p>0` unfolding divide_le_eq_1 by auto
     hence d_fz_z:"d \<le> norm (f z - z)" apply(drule_tac d) .
     case goal1 hence as:"\<forall>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar> < d / real n" using `n>0` by(auto simp add:not_le)
-    have "norm (f z - z) \<le> (\<Sum>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar>)" unfolding euclidean_component.diff[THEN sym] by(rule norm_le_l1)
+    have "norm (f z - z) \<le> (\<Sum>i<DIM('a). \<bar>f z $$ i - z $$ i\<bar>)" unfolding euclidean_component_diff[THEN sym] by(rule norm_le_l1)
     also have "\<dots> < (\<Sum>i<DIM('a). d / real n)" apply(rule setsum_strict_mono) using as by auto
     also have "\<dots> = d" unfolding real_eq_of_nat n_def using n using DIM_positive[where 'a='a] by auto
     finally show False using d_fz_z by auto qed then guess i .. note i=this
@@ -1276,15 +1276,15 @@
   def r' \<equiv> "(\<chi>\<chi> i. real (r (b' i)) / real p)::'a"
   have "\<And>i. i<DIM('a) \<Longrightarrow> r (b' i) \<le> p" apply(rule order_trans) apply(rule rs(1)[OF b'_im,THEN conjunct2])
     using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
-  hence "r' \<in> {0..\<chi>\<chi> i. 1}"  unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+  hence "r' \<in> {0..\<chi>\<chi> i. 1}"  unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
     apply (simp only: if_P)
     apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
   def s' \<equiv> "(\<chi>\<chi> i. real (s (b' i)) / real p)::'a"
   have "\<And>i. i<DIM('a) \<Longrightarrow> s (b' i) \<le> p" apply(rule order_trans) apply(rule rs(2)[OF b'_im,THEN conjunct2])
     using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
-  hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+  hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
     apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
-  have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
+  have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
     apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using q(1)[rule_format,OF b'_im] `p>0` by(auto intro:less_imp_le)
   have *:"\<And>x. 1 + real x = real (Suc x)" by auto
   { have "(\<Sum>i<DIM('a). \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>i<DIM('a). 1)" 

--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -1523,7 +1523,7 @@
   have ***:"\<And>y y1 y2 d dx::real. (y1\<le>y\<and>y2\<le>y) \<or> (y\<le>y1\<and>y\<le>y2) \<Longrightarrow> d < abs dx \<Longrightarrow> abs(y1 - y - - dx) \<le> d \<Longrightarrow> (abs (y2 - y - dx) \<le> d) \<Longrightarrow> False" by arith
   show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"]) 
     using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
-    unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
+    unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
 qed
 
 subsection {* Lemmas for working on @{typ "real^1"} *}

--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -18,7 +18,7 @@
 (* ------------------------------------------------------------------------- *)
 
 lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
-  by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
+  by (metis linear_conv_bounded_linear bounded_linear_scaleR_right)
 
 lemma injective_scaleR: 
 assumes "(c :: real) ~= 0"
@@ -128,7 +128,7 @@
 proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
   have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
   have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
-    unfolding euclidean_component.setsum euclidean_scaleR basis_component *
+    unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
     apply(rule setsum_cong2) using assms by auto
   show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
 qed
@@ -1175,7 +1175,7 @@
     have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
     have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
       apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
-    also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
+    also have "\<dots> \<le> 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto
     finally 
     show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
       apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
@@ -2229,7 +2229,7 @@
     have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
     have "x : affine hull S" using assms hull_subset[of S] by auto
     moreover have "1 / e + - ((1 - e) / e) = 1" 
-       using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
+       using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
     ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
         using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)     
     have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
@@ -2957,7 +2957,7 @@
   thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI)
     using True using DIM_positive[where 'a='a] by auto
 next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
-    apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
+    apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
 
 subsection {* Now set-to-set for closed/compact sets. *}
 
@@ -3053,7 +3053,7 @@
   apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
   apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
   apply(rule assms[unfolded convex_def, rule_format]) prefer 6
-  by (auto intro: tendsto_intros)
+  by (auto intro!: tendsto_intros)
 
 lemma convex_interior:
   fixes s :: "'a::real_normed_vector set"
@@ -3221,13 +3221,13 @@
   ultimately have "z \<in> convex hull {v \<in> c. u v \<le> 0}" unfolding convex_hull_explicit mem_Collect_eq
     apply(rule_tac x="{v \<in> c. u v < 0}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * - u y" in exI)
     using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def
-    by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
+    by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
   moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * u x" 
     apply (rule) apply (rule mult_nonneg_nonneg) using * by auto 
   hence "z \<in> convex hull {v \<in> c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq
     apply(rule_tac x="{v \<in> c. 0 < u v}" in exI, rule_tac x="\<lambda>y. inverse (setsum u {x\<in>c. u x > 0}) * u y" in exI)
     using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def using *
-    by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
+    by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
   ultimately show ?thesis apply(rule_tac x="{v\<in>c. u v \<le> 0}" in exI, rule_tac x="{v\<in>c. u v > 0}" in exI) by auto
 qed
 
@@ -4157,7 +4157,7 @@
   let ?D = "{..<DIM('a)}" let ?a = "setsum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) {(basis i) | i. i<DIM('a)}"
   have *:"{basis i :: 'a | i. i<DIM('a)} = basis ` ?D" by auto
   { fix i assume i:"i<DIM('a)" have "?a $$ i = inverse (2 * real DIM('a))"
-      unfolding euclidean_component.setsum * and setsum_reindex[OF basis_inj] and o_def
+      unfolding euclidean_component_setsum * and setsum_reindex[OF basis_inj] and o_def
       apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2)
       defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) }
   note ** = this
@@ -4270,7 +4270,7 @@
   { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
       unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
       apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) 
-      unfolding euclidean_component.setsum
+      unfolding euclidean_component_setsum
       apply(rule setsum_cong2)
       using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
       by (auto simp add: Euclidean_Space.basis_component[of i])}
@@ -4678,7 +4678,7 @@
          hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto
       def x2 == "z+ e2 *\<^sub>R (z-x)"
          hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto
-      have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp
+      have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp
       hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
          using x1_def x2_def apply (auto simp add: algebra_simps)
          using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -93,13 +93,13 @@
 proof -
   have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
     ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
-    by (intro Lim_cong_within) (auto simp add: divide.diff divide.add)
+    by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
   also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
     by (simp add: Lim_null[symmetric])
   also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
     by (intro Lim_cong_within) (simp_all add: field_simps)
   finally show ?thesis
-    by (simp add: mult.bounded_linear_right has_derivative_within)
+    by (simp add: bounded_linear_mult_right has_derivative_within)
 qed
 
 lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
@@ -140,10 +140,31 @@
   apply (simp add: local.scaleR local.diff local.add local.zero)
   done
 
+lemmas scaleR_right_has_derivative =
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
+
+lemmas scaleR_left_has_derivative =
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
+
+lemmas inner_right_has_derivative =
+  bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
+
+lemmas inner_left_has_derivative =
+  bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
+
+lemmas mult_right_has_derivative =
+  bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
+
+lemmas mult_left_has_derivative =
+  bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
+
+lemmas euclidean_component_has_derivative =
+  bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
+
 lemma has_derivative_neg:
   assumes "(f has_derivative f') net"
   shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
-  using scaleR_right.has_derivative [where r="-1", OF assms] by auto
+  using scaleR_right_has_derivative [where r="-1", OF assms] by auto
 
 lemma has_derivative_add:
   assumes "(f has_derivative f') net" and "(g has_derivative g') net"
@@ -181,9 +202,9 @@
   has_derivative_id has_derivative_const
   has_derivative_add has_derivative_sub has_derivative_neg
   has_derivative_add_const
-  scaleR_left.has_derivative scaleR_right.has_derivative
-  inner_left.has_derivative inner_right.has_derivative
-  euclidean_component.has_derivative
+  scaleR_left_has_derivative scaleR_right_has_derivative
+  inner_left_has_derivative inner_right_has_derivative
+  euclidean_component_has_derivative
 
 subsubsection {* Limit transformation for derivatives *}
 
@@ -459,7 +480,7 @@
   "f differentiable net \<Longrightarrow>
   (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
   unfolding differentiable_def
-  apply(erule exE, drule scaleR_right.has_derivative) by auto
+  apply(erule exE, drule scaleR_right_has_derivative) by auto
 
 lemma differentiable_neg [intro]:
   "f differentiable net \<Longrightarrow>
@@ -693,7 +714,7 @@
   show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\<bar>?D k $$ j\<bar> / 2 * \<bar>d\<bar>"])
     using *[of "-d"] and *[of d] and d[THEN conjunct1] and j
     unfolding mult_minus_left
-    unfolding abs_mult diff_minus_eq_add scaleR.minus_left
+    unfolding abs_mult diff_minus_eq_add scaleR_minus_left
     unfolding algebra_simps by (auto intro: mult_pos_pos)
 qed
 
@@ -769,7 +790,7 @@
     fix x assume x:"x \<in> {a<..<b}"
     show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
       by (intro has_derivative_intros assms(3)[rule_format,OF x]
-        mult_right.has_derivative)
+        mult_right_has_derivative)
   qed(insert assms(1), auto simp add:field_simps)
   then guess x ..
   thus ?thesis apply(rule_tac x=x in bexI)
@@ -1740,7 +1761,7 @@
 lemma has_vector_derivative_cmul:
   "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
   unfolding has_vector_derivative_def
-  apply (drule scaleR_right.has_derivative)
+  apply (drule scaleR_right_has_derivative)
   by (auto simp add: algebra_simps)
 
 lemma has_vector_derivative_cmul_eq:
@@ -1819,7 +1840,7 @@
   shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
   using assms(2) unfolding has_vector_derivative_def apply-
   apply(drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
-  unfolding o_def scaleR.scaleR_left by auto
+  unfolding o_def real_scaleR_def scaleR_scaleR .
 
 lemma vector_diff_chain_within:
   assumes "(f has_vector_derivative f') (at x within s)"
@@ -1827,6 +1848,6 @@
   shows "((g o f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
   using assms(2) unfolding has_vector_derivative_def apply-
   apply(drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
-  unfolding o_def scaleR.scaleR_left by auto
+  unfolding o_def real_scaleR_def scaleR_scaleR .
 
 end

--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -118,20 +118,38 @@
 lemma bounded_linear_euclidean_component:
   "bounded_linear (\<lambda>x. euclidean_component x i)"
   unfolding euclidean_component_def
-  by (rule inner.bounded_linear_right)
+  by (rule bounded_linear_inner_right)
+
+lemmas tendsto_euclidean_component [tendsto_intros] =
+  bounded_linear.tendsto [OF bounded_linear_euclidean_component]
+
+lemmas isCont_euclidean_component [simp] =
+  bounded_linear.isCont [OF bounded_linear_euclidean_component]
+
+lemma euclidean_component_zero: "0 $$ i = 0"
+  unfolding euclidean_component_def by (rule inner_zero_right)
 
-interpretation euclidean_component:
-  bounded_linear "\<lambda>x. euclidean_component x i"
-  by (rule bounded_linear_euclidean_component)
+lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
+  unfolding euclidean_component_def by (rule inner_add_right)
+
+lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
+  unfolding euclidean_component_def by (rule inner_diff_right)
 
-declare euclidean_component.isCont [simp]
+lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
+  unfolding euclidean_component_def by (rule inner_minus_right)
+
+lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
+  unfolding euclidean_component_def by (rule inner_scaleR_right)
+
+lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
+  unfolding euclidean_component_def by (rule inner_setsum_right)
 
 lemma euclidean_eqI:
   fixes x y :: "'a::euclidean_space"
   assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
 proof -
   from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
-    by (simp add: euclidean_component.diff)
+    by (simp add: euclidean_component_diff)
   then show "x = y"
     unfolding euclidean_component_def euclidean_all_zero by simp
 qed
@@ -153,23 +171,19 @@
   assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
   unfolding euclidean_component_def basis_zero[OF assms] by simp
 
-lemma euclidean_scaleR:
-  shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
-  unfolding euclidean_component_def by auto
-
 lemmas euclidean_simps =
-  euclidean_component.add
-  euclidean_component.diff
-  euclidean_scaleR
-  euclidean_component.minus
-  euclidean_component.setsum
+  euclidean_component_add
+  euclidean_component_diff
+  euclidean_component_scaleR
+  euclidean_component_minus
+  euclidean_component_setsum
   basis_component
 
 lemma euclidean_representation:
   fixes x :: "'a::euclidean_space"
   shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
   apply (rule euclidean_eqI)
-  apply (simp add: euclidean_component.setsum euclidean_component.scaleR)
+  apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
   apply (simp add: if_distrib setsum_delta cong: if_cong)
   done
 
@@ -180,7 +194,7 @@
 
 lemma euclidean_lambda_beta [simp]:
   "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
-  by (auto simp: euclidean_component.setsum euclidean_component.scaleR
+  by (auto simp: euclidean_component_setsum euclidean_component_scaleR
     Chi_def if_distrib setsum_cases intro!: setsum_cong)
 
 lemma euclidean_lambda_beta':
@@ -201,7 +215,7 @@
 lemma euclidean_inner:
   "inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))"
   by (subst (1 2) euclidean_representation,
-    simp add: inner_left.setsum inner_right.setsum
+    simp add: inner_setsum_left inner_setsum_right
     dot_basis if_distrib setsum_cases mult_commute)
 
 lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"

--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -66,7 +66,7 @@
     apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
     have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
     thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
-      unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def
+      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
       unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
   note lem3 = this[rule_format]
   have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto

--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -401,14 +401,15 @@
 unfolding norm_vec_def
 by (rule member_le_setL2) simp_all
 
-interpretation vec_nth: bounded_linear "\<lambda>x. x $ i"
+lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
 apply default
 apply (rule vector_add_component)
 apply (rule vector_scaleR_component)
 apply (rule_tac x="1" in exI, simp add: norm_nth_le)
 done
 
-declare vec_nth.isCont [simp]
+lemmas isCont_vec_nth [simp] =
+  bounded_linear.isCont [OF bounded_linear_vec_nth]
 
 instance vec :: (banach, finite) banach ..
 

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -16,7 +16,7 @@
 
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
-  scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
+  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
 
 lemma real_arch_invD:
   "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
@@ -1225,7 +1225,7 @@
 lemma has_integral_cmul:
   shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
   unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
-  by(rule scaleR.bounded_linear_right)
+  by(rule bounded_linear_scaleR_right)
 
 lemma has_integral_neg:
   shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
@@ -2262,7 +2262,7 @@
   assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. norm(f x - g x) \<le> e"
   shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - setsum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le> e * content({a..b})"
   apply(rule order_trans[OF _ rsum_bound[OF assms]]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
-  unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR.diff_right by auto
+  unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR_diff_right by auto
 
 lemma has_integral_bound: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "0 \<le> B" "(f has_integral i) ({a..b})" "\<forall>x\<in>{a..b}. norm(f x) \<le> B"
@@ -2287,7 +2287,7 @@
 lemma rsum_component_le: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. (f x)$$i \<le> (g x)$$i"
   shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)$$i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)$$i"
-  unfolding  euclidean_component.setsum apply(rule setsum_mono) apply safe
+  unfolding  euclidean_component_setsum apply(rule setsum_mono) apply safe
 proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
   from this(3) guess u v apply-by(erule exE)+ note b=this
   show "(content b *\<^sub>R f a) $$ i \<le> (content b *\<^sub>R g a) $$ i" unfolding b
@@ -2988,7 +2988,7 @@
       have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
         norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
         apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
-        unfolding scaleR.diff_left by(auto simp add:algebra_simps)
+        unfolding scaleR_diff_left by(auto simp add:algebra_simps)
       also have "... \<le> e * norm (u - x) + e * norm (v - x)"
         apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4
         apply(rule d(2)[of "x" "v",unfolded o_def])
@@ -3123,7 +3123,7 @@
   assumes "continuous_on {a..b} f" "x \<in> {a..b}"
   shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
   unfolding has_vector_derivative_def has_derivative_within_alt
-apply safe apply(rule scaleR.bounded_linear_left)
+apply safe apply(rule bounded_linear_scaleR_left)
 proof- fix e::real assume e:"e>0"
   note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def]
   from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format]
@@ -3223,8 +3223,8 @@
        have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel
         unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
         apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
-      also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR.diff_right scaleR.scaleR_left[THEN sym]
-        unfolding real_scaleR_def using assms(1) by auto finally have *:"?l = ?r" .
+      also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR
+        using assms(1) by auto finally have *:"?l = ?r" .
       show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" using ** unfolding * unfolding norm_scaleR
         using assms(1) by(auto simp add:field_simps) qed qed qed
 
@@ -3256,7 +3256,7 @@
 lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \<noteq> 0"
   shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` {a..b})"
   apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq[where 'a='a]
-  unfolding scaleR_right_distrib euclidean_simps scaleR.scaleR_left[THEN sym]
+  unfolding scaleR_right_distrib euclidean_simps scaleR_scaleR
   defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps)
   apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto
 
@@ -3442,7 +3442,7 @@
     show ?case unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[THEN sym] split_minus
       unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)]
     proof(rule norm_triangle_le,rule **) 
-      case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst divide.setsum)
+      case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib)
       proof(rule order_refl,safe,unfold not_le o_def split_conv fst_conv,rule ccontr) fix x k assume as:"(x,k) \<in> p"
           "e * (interval_upperbound k -  interval_lowerbound k) / 2
           < norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))"
@@ -4159,7 +4159,7 @@
       "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
       "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)" 
       unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg)
-      apply safe unfolding real_scaleR_def mult.diff_right[THEN sym]
+      apply safe unfolding real_scaleR_def right_diff_distrib[THEN sym]
       apply(rule_tac[!] mult_nonneg_nonneg)
     proof- fix a b assume ab:"(a,b) \<in> p1"
       show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
@@ -4535,7 +4535,7 @@
          show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"])
            unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule norm_setsum)
            apply(rule setsum_mono) unfolding split_paired_all split_conv
-           unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym]
+           unfolding split_def setsum_left_distrib[THEN sym] scaleR_diff_right[THEN sym]
            unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
          proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto
            from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this
@@ -5202,7 +5202,7 @@
 proof- have *:"\<And>x. ((\<chi>\<chi> i. abs(f x$$i))::'c::ordered_euclidean_space) = (setsum (\<lambda>i.
     (((\<lambda>y. (\<chi>\<chi> j. if j = i then y else 0)) o
     (((\<lambda>x. (norm((\<chi>\<chi> j. if j = i then x$$i else 0)::'c::ordered_euclidean_space))) o f))) x)) {..<DIM('c)})"
-    unfolding euclidean_eq[where 'a='c] euclidean_component.setsum apply safe
+    unfolding euclidean_eq[where 'a='c] euclidean_component_setsum apply safe
     unfolding euclidean_lambda_beta'
   proof- case goal1 have *:"\<And>i xa. ((if i = xa then f x $$ xa else 0) * (if i = xa then f x $$ xa else 0)) =
       (if i = xa then (f x $$ xa) * (f x $$ xa) else 0)" by auto
@@ -5220,7 +5220,7 @@
     apply(rule absolutely_integrable_linear) unfolding o_def apply(rule absolutely_integrable_norm)
     apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear
     apply(rule_tac[!] linearI) unfolding euclidean_eq[where 'a='c]
-    by(auto simp:euclidean_scaleR[where 'a=real,unfolded real_scaleR_def])
+    by(auto simp:euclidean_component_scaleR[where 'a=real,unfolded real_scaleR_def])
 qed
 
 lemma absolutely_integrable_max: fixes f g::"'m::ordered_euclidean_space \<Rightarrow> 'n::ordered_euclidean_space"
@@ -5266,7 +5266,7 @@
     proof- fix k and i assume "k\<in>d" and i:"i<DIM('m)"
       from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this
       show "\<bar>integral k f $$ i\<bar> \<le> integral k (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ i" apply(rule abs_leI)
-        unfolding euclidean_component.minus[THEN sym] defer apply(subst integral_neg[THEN sym])
+        unfolding euclidean_component_minus[THEN sym] defer apply(subst integral_neg[THEN sym])
         defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg)
         using integrable_on_subinterval[OF assms(1),of a b]
           integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto
@@ -5276,7 +5276,7 @@
         using integrable_on_subdivision[OF d assms(2)] by auto
       have "(\<Sum>i\<in>d. integral i (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j)
         = integral (\<Union>d) (\<lambda>x. (\<chi>\<chi> j. abs(f x$$j)) ::'m::ordered_euclidean_space) $$ j"
-        unfolding euclidean_component.setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
+        unfolding euclidean_component_setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
       also have "... \<le> integral UNIV (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j"
         apply(rule integral_subset_component_le) using assms * by auto
       finally show ?case .

--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -198,8 +198,8 @@
 
 text{* Dot product in terms of the norm rather than conversely. *}
 
-lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left 
-inner.scaleR_left inner.scaleR_right
+lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left 
+inner_scaleR_left inner_scaleR_right
 
 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
   unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
@@ -1558,7 +1558,7 @@
   unfolding independent_eq_inj_on [OF basis_inj]
   apply clarify
   apply (drule_tac f="inner (basis a)" in arg_cong)
-  apply (simp add: inner_right.setsum dot_basis)
+  apply (simp add: inner_setsum_right dot_basis)
   done
 
 lemma dimensionI:
@@ -1663,10 +1663,10 @@
     have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
     have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
       using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]
-      unfolding euclidean_component.setsum by(auto intro: abs_le_D1)
+      unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
     have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
       using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]
-      unfolding euclidean_component.setsum euclidean_component.minus
+      unfolding euclidean_component_setsum euclidean_component_minus
       by(auto simp add: setsum_negf intro: abs_le_D1)
     have "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn"
       apply (subst thp)
@@ -1756,7 +1756,7 @@
   have Kp: "?K > 0" by arith
     { assume C: "B < 0"
       have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
-        by(auto intro!:exI[where x=0] simp add:euclidean_component.zero)
+        by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
       hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
       with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
         by (simp add: mult_less_0_iff)
@@ -2829,7 +2829,7 @@
     unfolding infnorm_def
     unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
     unfolding infnorm_set_image ball_simps
-    apply(subst (1) euclidean_eq) unfolding euclidean_component.zero
+    apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
     by auto
   then show ?thesis using infnorm_pos_le[of x] by simp
 qed
@@ -2881,7 +2881,7 @@
 lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \<bar>a\<bar> * infnorm x"
   apply (subst infnorm_def)
   unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
-  unfolding infnorm_set_image ball_simps euclidean_scaleR abs_mult
+  unfolding infnorm_set_image ball_simps euclidean_component_scaleR abs_mult
   using component_le_infnorm[of x] by(auto intro: mult_mono) 
 
 lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -14,7 +14,7 @@
 
 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
   unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
-  apply(auto simp add:power2_eq_square) unfolding euclidean_component.diff ..
+  apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
 
 lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
   apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
@@ -1912,7 +1912,7 @@
   fixes S :: "'a::real_normed_vector set"
   shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
   apply (rule bounded_linear_image, assumption)
-  apply (rule scaleR.bounded_linear_right)
+  apply (rule bounded_linear_scaleR_right)
   done
 
 lemma bounded_translation:
@@ -3537,7 +3537,7 @@
 proof-
   { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
     hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
-      using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
+      using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
       unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
   }
   thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
@@ -4365,7 +4365,7 @@
   assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
 proof-
   let ?f = "\<lambda>x. scaleR c x"
-  have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
+  have *:"bounded_linear ?f" by (rule bounded_linear_scaleR_right)
   show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
     using linear_continuous_at[OF *] assms by auto
 qed
@@ -4951,7 +4951,7 @@
         unfolding Lim_sequentially by(auto simp add: dist_norm)
       hence "(f ---> x) sequentially" unfolding f_def
         using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
-        using scaleR.tendsto [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto  }
+        using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto  }
     ultimately have "x \<in> closure {a<..<b}"
       using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto  }
   thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
@@ -5571,7 +5571,7 @@
 subsection {* Some properties of a canonical subspace *}
 
 (** move **)
-declare euclidean_component.zero[simp]  
+declare euclidean_component_zero[simp]
 
 lemma subspace_substandard:
   "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
@@ -6027,15 +6027,15 @@
 
 lemmas Lim_ident_at = LIM_ident
 lemmas Lim_const = tendsto_const
-lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
+lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
 lemmas Lim_neg = tendsto_minus
 lemmas Lim_add = tendsto_add
 lemmas Lim_sub = tendsto_diff
-lemmas Lim_mul = scaleR.tendsto
-lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
+lemmas Lim_mul = tendsto_scaleR
+lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
 lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
 lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
-lemmas Lim_component = euclidean_component.tendsto
+lemmas Lim_component = tendsto_euclidean_component
 lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
 
 end

--- a/src/HOL/Probability/Borel_Space.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -816,7 +816,7 @@
   proof cases
     assume "b \<noteq> 0"
     with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
-      by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
+      by (auto intro!: open_affinity simp: scaleR_add_right mem_def)
     hence "?S \<in> sets borel"
       unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
     moreover

--- a/src/HOL/Probability/Independent_Family.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -563,7 +563,7 @@
     with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))"
       by simp
     moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"
-      by (intro mult_right.sums finite_measure_UNION F dis)
+      by (intro sums_mult finite_measure_UNION F dis)
     ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"
       by (auto dest!: sums_unique)
     with F show "(\<Union>i. F i) \<in> sets ?D"

--- a/src/HOL/RealVector.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/RealVector.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -62,24 +62,28 @@
   and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
   and scale_left_diff_distrib [algebra_simps]:
         "scale (a - b) x = scale a x - scale b x"
+  and scale_setsum_left: "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)"
 proof -
   interpret s: additive "\<lambda>a. scale a x"
     proof qed (rule scale_left_distrib)
   show "scale 0 x = 0" by (rule s.zero)
   show "scale (- a) x = - (scale a x)" by (rule s.minus)
   show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
+  show "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" by (rule s.setsum)
 qed
 
 lemma scale_zero_right [simp]: "scale a 0 = 0"
   and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
   and scale_right_diff_distrib [algebra_simps]:
         "scale a (x - y) = scale a x - scale a y"
+  and scale_setsum_right: "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))"
 proof -
   interpret s: additive "\<lambda>x. scale a x"
     proof qed (rule scale_right_distrib)
   show "scale a 0 = 0" by (rule s.zero)
   show "scale a (- x) = - (scale a x)" by (rule s.minus)
   show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
+  show "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" by (rule s.setsum)
 qed
 
 lemma scale_eq_0_iff [simp]:
@@ -140,16 +144,16 @@
 end
 
 class real_vector = scaleR + ab_group_add +
-  assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
-  and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
+  assumes scaleR_add_right: "scaleR a (x + y) = scaleR a x + scaleR a y"
+  and scaleR_add_left: "scaleR (a + b) x = scaleR a x + scaleR b x"
   and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
   and scaleR_one: "scaleR 1 x = x"
 
 interpretation real_vector:
   vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
 apply unfold_locales
-apply (rule scaleR_right_distrib)
-apply (rule scaleR_left_distrib)
+apply (rule scaleR_add_right)
+apply (rule scaleR_add_left)
 apply (rule scaleR_scaleR)
 apply (rule scaleR_one)
 done
@@ -159,16 +163,25 @@
 lemmas scaleR_left_commute = real_vector.scale_left_commute
 lemmas scaleR_zero_left = real_vector.scale_zero_left
 lemmas scaleR_minus_left = real_vector.scale_minus_left
-lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib
+lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib
+lemmas scaleR_setsum_left = real_vector.scale_setsum_left
 lemmas scaleR_zero_right = real_vector.scale_zero_right
 lemmas scaleR_minus_right = real_vector.scale_minus_right
-lemmas scaleR_right_diff_distrib = real_vector.scale_right_diff_distrib
+lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib
+lemmas scaleR_setsum_right = real_vector.scale_setsum_right
 lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
 lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
 lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
 lemmas scaleR_cancel_left = real_vector.scale_cancel_left
 lemmas scaleR_cancel_right = real_vector.scale_cancel_right
 
+text {* Legacy names *}
+
+lemmas scaleR_left_distrib = scaleR_add_left
+lemmas scaleR_right_distrib = scaleR_add_right
+lemmas scaleR_left_diff_distrib = scaleR_diff_left
+lemmas scaleR_right_diff_distrib = scaleR_diff_right
+
 lemma scaleR_minus1_left [simp]:
   fixes x :: "'a::real_vector"
   shows "scaleR (-1) x = - x"
@@ -1059,8 +1072,8 @@
 
 end
 
-interpretation mult:
-  bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
+lemma bounded_bilinear_mult:
+  "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
 apply (rule bounded_bilinear.intro)
 apply (rule left_distrib)
 apply (rule right_distrib)
@@ -1070,19 +1083,21 @@
 apply (simp add: norm_mult_ineq)
 done
 
-interpretation mult_left:
-  bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
-by (rule mult.bounded_linear_left)
+lemma bounded_linear_mult_left:
+  "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
+  using bounded_bilinear_mult
+  by (rule bounded_bilinear.bounded_linear_left)
 
-interpretation mult_right:
-  bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
-by (rule mult.bounded_linear_right)
+lemma bounded_linear_mult_right:
+  "bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)"
+  using bounded_bilinear_mult
+  by (rule bounded_bilinear.bounded_linear_right)
 
-interpretation divide:
-  bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
-unfolding divide_inverse by (rule mult.bounded_linear_left)
+lemma bounded_linear_divide:
+  "bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
+  unfolding divide_inverse by (rule bounded_linear_mult_left)
 
-interpretation scaleR: bounded_bilinear "scaleR"
+lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
 apply (rule bounded_bilinear.intro)
 apply (rule scaleR_left_distrib)
 apply (rule scaleR_right_distrib)
@@ -1091,14 +1106,16 @@
 apply (rule_tac x="1" in exI, simp)
 done
 
-interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
-by (rule scaleR.bounded_linear_left)
+lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
+  using bounded_bilinear_scaleR
+  by (rule bounded_bilinear.bounded_linear_left)
 
-interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
-by (rule scaleR.bounded_linear_right)
+lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)"
+  using bounded_bilinear_scaleR
+  by (rule bounded_bilinear.bounded_linear_right)
 
-interpretation of_real: bounded_linear "\<lambda>r. of_real r"
-unfolding of_real_def by (rule scaleR.bounded_linear_left)
+lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
+  unfolding of_real_def by (rule bounded_linear_scaleR_left)
 
 subsection{* Hausdorff and other separation properties *}
 

--- a/src/HOL/SEQ.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/SEQ.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -377,7 +377,7 @@
 lemma LIMSEQ_mult:
   fixes a b :: "'a::real_normed_algebra"
   shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
-by (rule mult.tendsto)
+  by (rule tendsto_mult)
 
 lemma increasing_LIMSEQ:
   fixes f :: "nat \<Rightarrow> real"

--- a/src/HOL/Series.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Series.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -211,50 +211,54 @@
   "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
 by (intro sums_unique sums summable_sums)
 
+lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real]
+lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
+lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
+
 lemma sums_mult:
   fixes c :: "'a::real_normed_algebra"
   shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
-by (rule mult_right.sums)
+  by (rule bounded_linear.sums [OF bounded_linear_mult_right])
 
 lemma summable_mult:
   fixes c :: "'a::real_normed_algebra"
   shows "summable f \<Longrightarrow> summable (%n. c * f n)"
-by (rule mult_right.summable)
+  by (rule bounded_linear.summable [OF bounded_linear_mult_right])
 
 lemma suminf_mult:
   fixes c :: "'a::real_normed_algebra"
   shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"
-by (rule mult_right.suminf [symmetric])
+  by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric])
 
 lemma sums_mult2:
   fixes c :: "'a::real_normed_algebra"
   shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
-by (rule mult_left.sums)
+  by (rule bounded_linear.sums [OF bounded_linear_mult_left])
 
 lemma summable_mult2:
   fixes c :: "'a::real_normed_algebra"
   shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
-by (rule mult_left.summable)
+  by (rule bounded_linear.summable [OF bounded_linear_mult_left])
 
 lemma suminf_mult2:
   fixes c :: "'a::real_normed_algebra"
   shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
-by (rule mult_left.suminf)
+  by (rule bounded_linear.suminf [OF bounded_linear_mult_left])
 
 lemma sums_divide:
   fixes c :: "'a::real_normed_field"
   shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
-by (rule divide.sums)
+  by (rule bounded_linear.sums [OF bounded_linear_divide])
 
 lemma summable_divide:
   fixes c :: "'a::real_normed_field"
   shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
-by (rule divide.summable)
+  by (rule bounded_linear.summable [OF bounded_linear_divide])
 
 lemma suminf_divide:
   fixes c :: "'a::real_normed_field"
   shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
-by (rule divide.suminf [symmetric])
+  by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
 
 lemma sums_add:
   fixes a b :: "'a::real_normed_field"
@@ -423,7 +427,7 @@
     by auto
   have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
     by simp
-  thus ?thesis using divide.sums [OF 2, of 2]
+  thus ?thesis using sums_divide [OF 2, of 2]
     by simp
 qed
 

--- a/src/HOL/Transcendental.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Transcendental.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -971,7 +971,7 @@
 
 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
 unfolding exp_def
-apply (subst of_real.suminf)
+apply (subst suminf_of_real)
 apply (rule summable_exp_generic)
 apply (simp add: scaleR_conv_of_real)
 done