remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
authorhuffman
Thu Aug 18 13:36:58 2011 -0700 (2011-08-18)
changeset 44282f0de18b62d63
parent 44275 d995733b635d
child 44283 637297cf6142
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
NEWS
src/HOL/Import/HOLLightReal.thy
src/HOL/Library/Convex.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/RealVector.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/NEWS	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -199,6 +199,19 @@
     1.4    tendsto_vector   ~> vec_tendstoI
     1.5    Cauchy_vector    ~> vec_CauchyI
     1.6  
     1.7 +* Complex_Main: The locale interpretations for the bounded_linear and
     1.8 +bounded_bilinear locales have been removed, in order to reduce the
     1.9 +number of duplicate lemmas. Users must use the original names for
    1.10 +distributivity theorems, potential INCOMPATIBILITY.
    1.11 +
    1.12 +  divide.add ~> add_divide_distrib
    1.13 +  divide.diff ~> diff_divide_distrib
    1.14 +  divide.setsum ~> setsum_divide_distrib
    1.15 +  mult.add_right ~> right_distrib
    1.16 +  mult.diff_right ~> right_diff_distrib
    1.17 +  mult_right.setsum ~> setsum_right_distrib
    1.18 +  mult_left.diff ~> left_diff_distrib
    1.19 +
    1.20  
    1.21  *** Document preparation ***
    1.22  
     2.1 --- a/src/HOL/Import/HOLLightReal.thy	Thu Aug 18 17:42:35 2011 +0200
     2.2 +++ b/src/HOL/Import/HOLLightReal.thy	Thu Aug 18 13:36:58 2011 -0700
     2.3 @@ -112,7 +112,7 @@
     2.4  
     2.5  lemma REAL_DIFFSQ:
     2.6    "((x :: real) + y) * (x - y) = x * x - y * y"
     2.7 -  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult)
     2.8 +  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
     2.9  
    2.10  lemma REAL_ABS_TRIANGLE_LE:
    2.11    "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
    2.12 @@ -295,7 +295,7 @@
    2.13     (\<forall>(x :: real). 0 * x = 0) \<and>
    2.14     (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
    2.15     (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
    2.16 -  by (auto simp add: mult.add_right)
    2.17 +  by (auto simp add: right_distrib)
    2.18  
    2.19  lemma REAL_COMPLETE:
    2.20    "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
     3.1 --- a/src/HOL/Library/Convex.thy	Thu Aug 18 17:42:35 2011 +0200
     3.2 +++ b/src/HOL/Library/Convex.thy	Thu Aug 18 13:36:58 2011 -0700
     3.3 @@ -129,7 +129,7 @@
     3.4      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     3.5      hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
     3.6      hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
     3.7 -    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
     3.8 +    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     3.9      from this asms
    3.10      have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
    3.11      hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
    3.12 @@ -410,7 +410,7 @@
    3.13      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
    3.14      hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
    3.15      hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
    3.16 -    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
    3.17 +    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
    3.18      have "convex C" using asms by auto
    3.19      hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
    3.20        using asms convex_setsum[OF `finite s`
    3.21 @@ -433,7 +433,7 @@
    3.22        using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
    3.23          OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
    3.24      also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
    3.25 -      unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
    3.26 +      unfolding setsum_right_distrib[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
    3.27      also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
    3.28      also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
    3.29      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))"
     4.1 --- a/src/HOL/Library/FrechetDeriv.thy	Thu Aug 18 17:42:35 2011 +0200
     4.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Thu Aug 18 13:36:58 2011 -0700
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Frechet Derivative *}
     4.5  
     4.6  theory FrechetDeriv
     4.7 -imports Lim Complex_Main
     4.8 +imports Complex_Main
     4.9  begin
    4.10  
    4.11  definition
    4.12 @@ -398,9 +398,11 @@
    4.13      by (simp only: FDERIV_lemma)
    4.14  qed
    4.15  
    4.16 -lemmas FDERIV_mult = mult.FDERIV
    4.17 +lemmas FDERIV_mult =
    4.18 +  bounded_bilinear.FDERIV [OF bounded_bilinear_mult]
    4.19  
    4.20 -lemmas FDERIV_scaleR = scaleR.FDERIV
    4.21 +lemmas FDERIV_scaleR =
    4.22 +  bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR]
    4.23  
    4.24  
    4.25  subsection {* Powers *}
    4.26 @@ -427,10 +429,10 @@
    4.27  subsection {* Inverse *}
    4.28  
    4.29  lemmas bounded_linear_mult_const =
    4.30 -  mult.bounded_linear_left [THEN bounded_linear_compose]
    4.31 +  bounded_linear_mult_left [THEN bounded_linear_compose]
    4.32  
    4.33  lemmas bounded_linear_const_mult =
    4.34 -  mult.bounded_linear_right [THEN bounded_linear_compose]
    4.35 +  bounded_linear_mult_right [THEN bounded_linear_compose]
    4.36  
    4.37  lemma FDERIV_inverse:
    4.38    fixes x :: "'a::real_normed_div_algebra"
    4.39 @@ -510,7 +512,7 @@
    4.40    fixes x :: "'a::real_normed_field" shows
    4.41    "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
    4.42   apply (unfold fderiv_def)
    4.43 - apply (simp add: mult.bounded_linear_left)
    4.44 + apply (simp add: bounded_linear_mult_left)
    4.45   apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
    4.46   apply (subst diff_divide_distrib)
    4.47   apply (subst times_divide_eq_left [symmetric])
     5.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Aug 18 17:42:35 2011 +0200
     5.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu Aug 18 13:36:58 2011 -0700
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Inner Product Spaces and the Gradient Derivative *}
     5.5  
     5.6  theory Inner_Product
     5.7 -imports Complex_Main FrechetDeriv
     5.8 +imports FrechetDeriv
     5.9  begin
    5.10  
    5.11  subsection {* Real inner product spaces *}
    5.12 @@ -43,6 +43,9 @@
    5.13  lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    5.14    by (simp add: diff_minus inner_add_left)
    5.15  
    5.16 +lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
    5.17 +  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    5.18 +
    5.19  text {* Transfer distributivity rules to right argument. *}
    5.20  
    5.21  lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    5.22 @@ -60,6 +63,9 @@
    5.23  lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    5.24    using inner_diff_left [of y z x] by (simp only: inner_commute)
    5.25  
    5.26 +lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    5.27 +  using inner_setsum_left [of f A x] by (simp only: inner_commute)
    5.28 +
    5.29  lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    5.30  lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    5.31  lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    5.32 @@ -148,8 +154,8 @@
    5.33  setup {* Sign.add_const_constraint
    5.34    (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
    5.35  
    5.36 -interpretation inner:
    5.37 -  bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
    5.38 +lemma bounded_bilinear_inner:
    5.39 +  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
    5.40  proof
    5.41    fix x y z :: 'a and r :: real
    5.42    show "inner (x + y) z = inner x z + inner y z"
    5.43 @@ -167,15 +173,20 @@
    5.44    qed
    5.45  qed
    5.46  
    5.47 -interpretation inner_left:
    5.48 -  bounded_linear "\<lambda>x::'a::real_inner. inner x y"
    5.49 -  by (rule inner.bounded_linear_left)
    5.50 +lemmas tendsto_inner [tendsto_intros] =
    5.51 +  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
    5.52 +
    5.53 +lemmas isCont_inner [simp] =
    5.54 +  bounded_bilinear.isCont [OF bounded_bilinear_inner]
    5.55  
    5.56 -interpretation inner_right:
    5.57 -  bounded_linear "\<lambda>y::'a::real_inner. inner x y"
    5.58 -  by (rule inner.bounded_linear_right)
    5.59 +lemmas FDERIV_inner =
    5.60 +  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
    5.61  
    5.62 -declare inner.isCont [simp]
    5.63 +lemmas bounded_linear_inner_left =
    5.64 +  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
    5.65 +
    5.66 +lemmas bounded_linear_inner_right =
    5.67 +  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
    5.68  
    5.69  
    5.70  subsection {* Class instances *}
    5.71 @@ -260,29 +271,29 @@
    5.72    by simp
    5.73  
    5.74  lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
    5.75 -  unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
    5.76 +  unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
    5.77  
    5.78  lemma GDERIV_add:
    5.79      "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
    5.80       \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
    5.81 -  unfolding gderiv_def inner_right.add by (rule FDERIV_add)
    5.82 +  unfolding gderiv_def inner_add_right by (rule FDERIV_add)
    5.83  
    5.84  lemma GDERIV_minus:
    5.85      "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
    5.86 -  unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
    5.87 +  unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
    5.88  
    5.89  lemma GDERIV_diff:
    5.90      "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
    5.91       \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
    5.92 -  unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
    5.93 +  unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
    5.94  
    5.95  lemma GDERIV_scaleR:
    5.96      "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
    5.97       \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
    5.98        :> (scaleR (f x) dg + scaleR df (g x))"
    5.99 -  unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
   5.100 +  unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
   5.101    apply (rule FDERIV_subst)
   5.102 -  apply (erule (1) scaleR.FDERIV)
   5.103 +  apply (erule (1) FDERIV_scaleR)
   5.104    apply (simp add: mult_ac)
   5.105    done
   5.106  
   5.107 @@ -306,7 +317,7 @@
   5.108    assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   5.109  proof -
   5.110    have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   5.111 -    by (intro inner.FDERIV FDERIV_ident)
   5.112 +    by (intro FDERIV_inner FDERIV_ident)
   5.113    have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   5.114      by (simp add: fun_eq_iff inner_commute)
   5.115    have "0 < inner x x" using `x \<noteq> 0` by simp
     6.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Aug 18 17:42:35 2011 +0200
     6.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Aug 18 13:36:58 2011 -0700
     6.3 @@ -489,11 +489,11 @@
     6.4  
     6.5  subsection {* Pair operations are linear *}
     6.6  
     6.7 -interpretation fst: bounded_linear fst
     6.8 +lemma bounded_linear_fst: "bounded_linear fst"
     6.9    using fst_add fst_scaleR
    6.10    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    6.11  
    6.12 -interpretation snd: bounded_linear snd
    6.13 +lemma bounded_linear_snd: "bounded_linear snd"
    6.14    using snd_add snd_scaleR
    6.15    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    6.16  
     7.1 --- a/src/HOL/Lim.thy	Thu Aug 18 17:42:35 2011 +0200
     7.2 +++ b/src/HOL/Lim.thy	Thu Aug 18 13:36:58 2011 -0700
     7.3 @@ -321,17 +321,23 @@
     7.4    "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
     7.5    by (rule tendsto_right_zero)
     7.6  
     7.7 -lemmas LIM_mult = mult.LIM
     7.8 +lemmas LIM_mult =
     7.9 +  bounded_bilinear.LIM [OF bounded_bilinear_mult]
    7.10  
    7.11 -lemmas LIM_mult_zero = mult.LIM_prod_zero
    7.12 +lemmas LIM_mult_zero =
    7.13 +  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
    7.14  
    7.15 -lemmas LIM_mult_left_zero = mult.LIM_left_zero
    7.16 +lemmas LIM_mult_left_zero =
    7.17 +  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
    7.18  
    7.19 -lemmas LIM_mult_right_zero = mult.LIM_right_zero
    7.20 +lemmas LIM_mult_right_zero =
    7.21 +  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
    7.22  
    7.23 -lemmas LIM_scaleR = scaleR.LIM
    7.24 +lemmas LIM_scaleR =
    7.25 +  bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
    7.26  
    7.27 -lemmas LIM_of_real = of_real.LIM
    7.28 +lemmas LIM_of_real =
    7.29 +  bounded_linear.LIM [OF bounded_linear_of_real]
    7.30  
    7.31  lemma LIM_power:
    7.32    fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    7.33 @@ -446,11 +452,11 @@
    7.34    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
    7.35    unfolding isCont_def by (rule LIM)
    7.36  
    7.37 -lemmas isCont_scaleR [simp] = scaleR.isCont
    7.38 +lemmas isCont_scaleR [simp] =
    7.39 +  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
    7.40  
    7.41 -lemma isCont_of_real [simp]:
    7.42 -  "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
    7.43 -  by (rule of_real.isCont)
    7.44 +lemmas isCont_of_real [simp] =
    7.45 +  bounded_linear.isCont [OF bounded_linear_of_real]
    7.46  
    7.47  lemma isCont_power [simp]:
    7.48    fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
     8.1 --- a/src/HOL/Limits.thy	Thu Aug 18 17:42:35 2011 +0200
     8.2 +++ b/src/HOL/Limits.thy	Thu Aug 18 13:36:58 2011 -0700
     8.3 @@ -510,9 +510,9 @@
     8.4    "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F"
     8.5    by (rule bounded_linear_right [THEN bounded_linear.Zfun])
     8.6  
     8.7 -lemmas Zfun_mult = mult.Zfun
     8.8 -lemmas Zfun_mult_right = mult.Zfun_right
     8.9 -lemmas Zfun_mult_left = mult.Zfun_left
    8.10 +lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
    8.11 +lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
    8.12 +lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
    8.13  
    8.14  
    8.15  subsection {* Limits *}
    8.16 @@ -752,7 +752,7 @@
    8.17  
    8.18  subsubsection {* Linear operators and multiplication *}
    8.19  
    8.20 -lemma (in bounded_linear) tendsto [tendsto_intros]:
    8.21 +lemma (in bounded_linear) tendsto:
    8.22    "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
    8.23    by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
    8.24  
    8.25 @@ -760,7 +760,7 @@
    8.26    "(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
    8.27    by (drule tendsto, simp only: zero)
    8.28  
    8.29 -lemma (in bounded_bilinear) tendsto [tendsto_intros]:
    8.30 +lemma (in bounded_bilinear) tendsto:
    8.31    "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) F"
    8.32    by (simp only: tendsto_Zfun_iff prod_diff_prod
    8.33                   Zfun_add Zfun Zfun_left Zfun_right)
    8.34 @@ -779,7 +779,14 @@
    8.35    "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) F"
    8.36    by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
    8.37  
    8.38 -lemmas tendsto_mult = mult.tendsto
    8.39 +lemmas tendsto_of_real [tendsto_intros] =
    8.40 +  bounded_linear.tendsto [OF bounded_linear_of_real]
    8.41 +
    8.42 +lemmas tendsto_scaleR [tendsto_intros] =
    8.43 +  bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]
    8.44 +
    8.45 +lemmas tendsto_mult [tendsto_intros] =
    8.46 +  bounded_bilinear.tendsto [OF bounded_bilinear_mult]
    8.47  
    8.48  lemma tendsto_power [tendsto_intros]:
    8.49    fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    8.50 @@ -897,7 +904,7 @@
    8.51    apply (erule (1) inverse_diff_inverse)
    8.52    apply (rule Zfun_minus)
    8.53    apply (rule Zfun_mult_left)
    8.54 -  apply (rule mult.Bfun_prod_Zfun)
    8.55 +  apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
    8.56    apply (erule (1) Bfun_inverse)
    8.57    apply (simp add: tendsto_Zfun_iff)
    8.58    done
    8.59 @@ -921,7 +928,7 @@
    8.60    fixes a b :: "'a::real_normed_field"
    8.61    shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
    8.62      \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
    8.63 -  by (simp add: mult.tendsto tendsto_inverse divide_inverse)
    8.64 +  by (simp add: tendsto_mult tendsto_inverse divide_inverse)
    8.65  
    8.66  lemma tendsto_sgn [tendsto_intros]:
    8.67    fixes l :: "'a::real_normed_vector"
     9.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Aug 18 17:42:35 2011 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Aug 18 13:36:58 2011 -0700
     9.3 @@ -1202,7 +1202,7 @@
     9.4        show "\<bar>(f z - z) $$ i\<bar> < d / real n" unfolding euclidean_simps proof(rule *)
     9.5          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
     9.6          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)"
     9.7 -          unfolding euclidean_component.diff[THEN sym] by(rule component_le_norm)+
     9.8 +          unfolding euclidean_component_diff[THEN sym] by(rule component_le_norm)+
     9.9          have tria:"norm (y - x) \<le> norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm]
    9.10            unfolding norm_minus_commute by auto
    9.11          also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto
    9.12 @@ -1234,7 +1234,7 @@
    9.13      assume as:"\<forall>i\<in>{1..n}. x i \<le> p" "i \<in> {1..n}"
    9.14      { assume "x i = p \<or> x i = 0" 
    9.15        have "(\<chi>\<chi> i. real (x (b' i)) / real p) \<in> {0::'a..\<chi>\<chi> i. 1}" unfolding mem_interval 
    9.16 -        apply safe unfolding euclidean_lambda_beta euclidean_component.zero
    9.17 +        apply safe unfolding euclidean_lambda_beta euclidean_component_zero
    9.18        proof (simp_all only: if_P) fix j assume j':"j<DIM('a)"
    9.19          hence j:"b' j \<in> {1..n}" using b' unfolding n_def bij_betw_def by auto
    9.20          show "0 \<le> real (x (b' j)) / real p"
    9.21 @@ -1262,11 +1262,11 @@
    9.22      have "\<forall>i<DIM('a). q (b' i) \<in> {0..<p}" using q(1) b'[unfolded bij_betw_def] by auto 
    9.23      hence "\<forall>i<DIM('a). q (b' i) \<in> {0..p}" apply-apply(rule,erule_tac x=i in allE) by auto
    9.24      hence "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta
    9.25 -      unfolding euclidean_component.zero apply (simp_all only: if_P)
    9.26 +      unfolding euclidean_component_zero apply (simp_all only: if_P)
    9.27        apply(rule divide_nonneg_pos) using `p>0` unfolding divide_le_eq_1 by auto
    9.28      hence d_fz_z:"d \<le> norm (f z - z)" apply(drule_tac d) .
    9.29      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)
    9.30 -    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)
    9.31 +    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)
    9.32      also have "\<dots> < (\<Sum>i<DIM('a). d / real n)" apply(rule setsum_strict_mono) using as by auto
    9.33      also have "\<dots> = d" unfolding real_eq_of_nat n_def using n using DIM_positive[where 'a='a] by auto
    9.34      finally show False using d_fz_z by auto qed then guess i .. note i=this
    9.35 @@ -1276,15 +1276,15 @@
    9.36    def r' \<equiv> "(\<chi>\<chi> i. real (r (b' i)) / real p)::'a"
    9.37    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])
    9.38      using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
    9.39 -  hence "r' \<in> {0..\<chi>\<chi> i. 1}"  unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
    9.40 +  hence "r' \<in> {0..\<chi>\<chi> i. 1}"  unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
    9.41      apply (simp only: if_P)
    9.42      apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto
    9.43    def s' \<equiv> "(\<chi>\<chi> i. real (s (b' i)) / real p)::'a"
    9.44    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])
    9.45      using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq)
    9.46 -  hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
    9.47 +  hence "s' \<in> {0..\<chi>\<chi> i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
    9.48      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
    9.49 -  have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero
    9.50 +  have "z\<in>{0..\<chi>\<chi> i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero
    9.51      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)
    9.52    have *:"\<And>x. 1 + real x = real (Suc x)" by auto
    9.53    { have "(\<Sum>i<DIM('a). \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>i<DIM('a). 1)" 
    10.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
    10.3 @@ -1523,7 +1523,7 @@
    10.4    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
    10.5    show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\<bar>D $ k $ j\<bar> / 2 * \<bar>d\<bar>"]) 
    10.6      using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left
    10.7 -    unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
    10.8 +    unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos)
    10.9  qed
   10.10  
   10.11  subsection {* Lemmas for working on @{typ "real^1"} *}
    11.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
    11.3 @@ -18,7 +18,7 @@
    11.4  (* ------------------------------------------------------------------------- *)
    11.5  
    11.6  lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
    11.7 -  by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
    11.8 +  by (metis linear_conv_bounded_linear bounded_linear_scaleR_right)
    11.9  
   11.10  lemma injective_scaleR: 
   11.11  assumes "(c :: real) ~= 0"
   11.12 @@ -128,7 +128,7 @@
   11.13  proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
   11.14    have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
   11.15    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)"
   11.16 -    unfolding euclidean_component.setsum euclidean_scaleR basis_component *
   11.17 +    unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
   11.18      apply(rule setsum_cong2) using assms by auto
   11.19    show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
   11.20  qed
   11.21 @@ -1175,7 +1175,7 @@
   11.22      have u2:"u2 \<le> 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto
   11.23      have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
   11.24        apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
   11.25 -    also have "\<dots> \<le> 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto
   11.26 +    also have "\<dots> \<le> 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto
   11.27      finally 
   11.28      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)
   11.29        apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
   11.30 @@ -2229,7 +2229,7 @@
   11.31      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)
   11.32      have "x : affine hull S" using assms hull_subset[of S] by auto
   11.33      moreover have "1 / e + - ((1 - e) / e) = 1" 
   11.34 -       using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
   11.35 +       using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
   11.36      ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
   11.37          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)     
   11.38      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)"
   11.39 @@ -2957,7 +2957,7 @@
   11.40    thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI)
   11.41      using True using DIM_positive[where 'a='a] by auto
   11.42  next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
   11.43 -    apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
   11.44 +    apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
   11.45  
   11.46  subsection {* Now set-to-set for closed/compact sets. *}
   11.47  
   11.48 @@ -3053,7 +3053,7 @@
   11.49    apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
   11.50    apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
   11.51    apply(rule assms[unfolded convex_def, rule_format]) prefer 6
   11.52 -  by (auto intro: tendsto_intros)
   11.53 +  by (auto intro!: tendsto_intros)
   11.54  
   11.55  lemma convex_interior:
   11.56    fixes s :: "'a::real_normed_vector set"
   11.57 @@ -3221,13 +3221,13 @@
   11.58    ultimately have "z \<in> convex hull {v \<in> c. u v \<le> 0}" unfolding convex_hull_explicit mem_Collect_eq
   11.59      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)
   11.60      using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def
   11.61 -    by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
   11.62 +    by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
   11.63    moreover have "\<forall>x\<in>{v \<in> c. 0 < u v}. 0 \<le> inverse (setsum u {x \<in> c. 0 < u x}) * u x" 
   11.64      apply (rule) apply (rule mult_nonneg_nonneg) using * by auto 
   11.65    hence "z \<in> convex hull {v \<in> c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq
   11.66      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)
   11.67      using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def using *
   11.68 -    by(auto simp add: setsum_negf mult_right.setsum[THEN sym])
   11.69 +    by(auto simp add: setsum_negf setsum_right_distrib[THEN sym])
   11.70    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
   11.71  qed
   11.72  
   11.73 @@ -4157,7 +4157,7 @@
   11.74    let ?D = "{..<DIM('a)}" let ?a = "setsum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) {(basis i) | i. i<DIM('a)}"
   11.75    have *:"{basis i :: 'a | i. i<DIM('a)} = basis ` ?D" by auto
   11.76    { fix i assume i:"i<DIM('a)" have "?a $$ i = inverse (2 * real DIM('a))"
   11.77 -      unfolding euclidean_component.setsum * and setsum_reindex[OF basis_inj] and o_def
   11.78 +      unfolding euclidean_component_setsum * and setsum_reindex[OF basis_inj] and o_def
   11.79        apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2)
   11.80        defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) }
   11.81    note ** = this
   11.82 @@ -4270,7 +4270,7 @@
   11.83    { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
   11.84        unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
   11.85        apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) 
   11.86 -      unfolding euclidean_component.setsum
   11.87 +      unfolding euclidean_component_setsum
   11.88        apply(rule setsum_cong2)
   11.89        using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2)
   11.90        by (auto simp add: Euclidean_Space.basis_component[of i])}
   11.91 @@ -4678,7 +4678,7 @@
   11.92           hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto
   11.93        def x2 == "z+ e2 *\<^sub>R (z-x)"
   11.94           hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto
   11.95 -      have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp
   11.96 +      have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp
   11.97        hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
   11.98           using x1_def x2_def apply (auto simp add: algebra_simps)
   11.99           using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto
    12.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Aug 18 17:42:35 2011 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Aug 18 13:36:58 2011 -0700
    12.3 @@ -93,13 +93,13 @@
    12.4  proof -
    12.5    have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) ---> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
    12.6      ((\<lambda>t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \<inter> I))"
    12.7 -    by (intro Lim_cong_within) (auto simp add: divide.diff divide.add)
    12.8 +    by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib)
    12.9    also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \<inter> I))"
   12.10      by (simp add: Lim_null[symmetric])
   12.11    also have "\<dots> \<longleftrightarrow> ((\<lambda>t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \<inter> I))"
   12.12      by (intro Lim_cong_within) (simp_all add: field_simps)
   12.13    finally show ?thesis
   12.14 -    by (simp add: mult.bounded_linear_right has_derivative_within)
   12.15 +    by (simp add: bounded_linear_mult_right has_derivative_within)
   12.16  qed
   12.17  
   12.18  lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
   12.19 @@ -140,10 +140,31 @@
   12.20    apply (simp add: local.scaleR local.diff local.add local.zero)
   12.21    done
   12.22  
   12.23 +lemmas scaleR_right_has_derivative =
   12.24 +  bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
   12.25 +
   12.26 +lemmas scaleR_left_has_derivative =
   12.27 +  bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
   12.28 +
   12.29 +lemmas inner_right_has_derivative =
   12.30 +  bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
   12.31 +
   12.32 +lemmas inner_left_has_derivative =
   12.33 +  bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
   12.34 +
   12.35 +lemmas mult_right_has_derivative =
   12.36 +  bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
   12.37 +
   12.38 +lemmas mult_left_has_derivative =
   12.39 +  bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
   12.40 +
   12.41 +lemmas euclidean_component_has_derivative =
   12.42 +  bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
   12.43 +
   12.44  lemma has_derivative_neg:
   12.45    assumes "(f has_derivative f') net"
   12.46    shows "((\<lambda>x. -(f x)) has_derivative (\<lambda>h. -(f' h))) net"
   12.47 -  using scaleR_right.has_derivative [where r="-1", OF assms] by auto
   12.48 +  using scaleR_right_has_derivative [where r="-1", OF assms] by auto
   12.49  
   12.50  lemma has_derivative_add:
   12.51    assumes "(f has_derivative f') net" and "(g has_derivative g') net"
   12.52 @@ -181,9 +202,9 @@
   12.53    has_derivative_id has_derivative_const
   12.54    has_derivative_add has_derivative_sub has_derivative_neg
   12.55    has_derivative_add_const
   12.56 -  scaleR_left.has_derivative scaleR_right.has_derivative
   12.57 -  inner_left.has_derivative inner_right.has_derivative
   12.58 -  euclidean_component.has_derivative
   12.59 +  scaleR_left_has_derivative scaleR_right_has_derivative
   12.60 +  inner_left_has_derivative inner_right_has_derivative
   12.61 +  euclidean_component_has_derivative
   12.62  
   12.63  subsubsection {* Limit transformation for derivatives *}
   12.64  
   12.65 @@ -459,7 +480,7 @@
   12.66    "f differentiable net \<Longrightarrow>
   12.67    (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
   12.68    unfolding differentiable_def
   12.69 -  apply(erule exE, drule scaleR_right.has_derivative) by auto
   12.70 +  apply(erule exE, drule scaleR_right_has_derivative) by auto
   12.71  
   12.72  lemma differentiable_neg [intro]:
   12.73    "f differentiable net \<Longrightarrow>
   12.74 @@ -693,7 +714,7 @@
   12.75    show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\<bar>?D k $$ j\<bar> / 2 * \<bar>d\<bar>"])
   12.76      using *[of "-d"] and *[of d] and d[THEN conjunct1] and j
   12.77      unfolding mult_minus_left
   12.78 -    unfolding abs_mult diff_minus_eq_add scaleR.minus_left
   12.79 +    unfolding abs_mult diff_minus_eq_add scaleR_minus_left
   12.80      unfolding algebra_simps by (auto intro: mult_pos_pos)
   12.81  qed
   12.82  
   12.83 @@ -769,7 +790,7 @@
   12.84      fix x assume x:"x \<in> {a<..<b}"
   12.85      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)"
   12.86        by (intro has_derivative_intros assms(3)[rule_format,OF x]
   12.87 -        mult_right.has_derivative)
   12.88 +        mult_right_has_derivative)
   12.89    qed(insert assms(1), auto simp add:field_simps)
   12.90    then guess x ..
   12.91    thus ?thesis apply(rule_tac x=x in bexI)
   12.92 @@ -1740,7 +1761,7 @@
   12.93  lemma has_vector_derivative_cmul:
   12.94    "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
   12.95    unfolding has_vector_derivative_def
   12.96 -  apply (drule scaleR_right.has_derivative)
   12.97 +  apply (drule scaleR_right_has_derivative)
   12.98    by (auto simp add: algebra_simps)
   12.99  
  12.100  lemma has_vector_derivative_cmul_eq:
  12.101 @@ -1819,7 +1840,7 @@
  12.102    shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
  12.103    using assms(2) unfolding has_vector_derivative_def apply-
  12.104    apply(drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
  12.105 -  unfolding o_def scaleR.scaleR_left by auto
  12.106 +  unfolding o_def real_scaleR_def scaleR_scaleR .
  12.107  
  12.108  lemma vector_diff_chain_within:
  12.109    assumes "(f has_vector_derivative f') (at x within s)"
  12.110 @@ -1827,6 +1848,6 @@
  12.111    shows "((g o f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
  12.112    using assms(2) unfolding has_vector_derivative_def apply-
  12.113    apply(drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
  12.114 -  unfolding o_def scaleR.scaleR_left by auto
  12.115 +  unfolding o_def real_scaleR_def scaleR_scaleR .
  12.116  
  12.117  end
    13.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
    13.3 @@ -118,20 +118,38 @@
    13.4  lemma bounded_linear_euclidean_component:
    13.5    "bounded_linear (\<lambda>x. euclidean_component x i)"
    13.6    unfolding euclidean_component_def
    13.7 -  by (rule inner.bounded_linear_right)
    13.8 +  by (rule bounded_linear_inner_right)
    13.9 +
   13.10 +lemmas tendsto_euclidean_component [tendsto_intros] =
   13.11 +  bounded_linear.tendsto [OF bounded_linear_euclidean_component]
   13.12 +
   13.13 +lemmas isCont_euclidean_component [simp] =
   13.14 +  bounded_linear.isCont [OF bounded_linear_euclidean_component]
   13.15 +
   13.16 +lemma euclidean_component_zero: "0 $$ i = 0"
   13.17 +  unfolding euclidean_component_def by (rule inner_zero_right)
   13.18  
   13.19 -interpretation euclidean_component:
   13.20 -  bounded_linear "\<lambda>x. euclidean_component x i"
   13.21 -  by (rule bounded_linear_euclidean_component)
   13.22 +lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
   13.23 +  unfolding euclidean_component_def by (rule inner_add_right)
   13.24 +
   13.25 +lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
   13.26 +  unfolding euclidean_component_def by (rule inner_diff_right)
   13.27  
   13.28 -declare euclidean_component.isCont [simp]
   13.29 +lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
   13.30 +  unfolding euclidean_component_def by (rule inner_minus_right)
   13.31 +
   13.32 +lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
   13.33 +  unfolding euclidean_component_def by (rule inner_scaleR_right)
   13.34 +
   13.35 +lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
   13.36 +  unfolding euclidean_component_def by (rule inner_setsum_right)
   13.37  
   13.38  lemma euclidean_eqI:
   13.39    fixes x y :: "'a::euclidean_space"
   13.40    assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
   13.41  proof -
   13.42    from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
   13.43 -    by (simp add: euclidean_component.diff)
   13.44 +    by (simp add: euclidean_component_diff)
   13.45    then show "x = y"
   13.46      unfolding euclidean_component_def euclidean_all_zero by simp
   13.47  qed
   13.48 @@ -153,23 +171,19 @@
   13.49    assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
   13.50    unfolding euclidean_component_def basis_zero[OF assms] by simp
   13.51  
   13.52 -lemma euclidean_scaleR:
   13.53 -  shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
   13.54 -  unfolding euclidean_component_def by auto
   13.55 -
   13.56  lemmas euclidean_simps =
   13.57 -  euclidean_component.add
   13.58 -  euclidean_component.diff
   13.59 -  euclidean_scaleR
   13.60 -  euclidean_component.minus
   13.61 -  euclidean_component.setsum
   13.62 +  euclidean_component_add
   13.63 +  euclidean_component_diff
   13.64 +  euclidean_component_scaleR
   13.65 +  euclidean_component_minus
   13.66 +  euclidean_component_setsum
   13.67    basis_component
   13.68  
   13.69  lemma euclidean_representation:
   13.70    fixes x :: "'a::euclidean_space"
   13.71    shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
   13.72    apply (rule euclidean_eqI)
   13.73 -  apply (simp add: euclidean_component.setsum euclidean_component.scaleR)
   13.74 +  apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
   13.75    apply (simp add: if_distrib setsum_delta cong: if_cong)
   13.76    done
   13.77  
   13.78 @@ -180,7 +194,7 @@
   13.79  
   13.80  lemma euclidean_lambda_beta [simp]:
   13.81    "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
   13.82 -  by (auto simp: euclidean_component.setsum euclidean_component.scaleR
   13.83 +  by (auto simp: euclidean_component_setsum euclidean_component_scaleR
   13.84      Chi_def if_distrib setsum_cases intro!: setsum_cong)
   13.85  
   13.86  lemma euclidean_lambda_beta':
   13.87 @@ -201,7 +215,7 @@
   13.88  lemma euclidean_inner:
   13.89    "inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))"
   13.90    by (subst (1 2) euclidean_representation,
   13.91 -    simp add: inner_left.setsum inner_right.setsum
   13.92 +    simp add: inner_setsum_left inner_setsum_right
   13.93      dot_basis if_distrib setsum_cases mult_commute)
   13.94  
   13.95  lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
    14.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Aug 18 17:42:35 2011 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Aug 18 13:36:58 2011 -0700
    14.3 @@ -66,7 +66,7 @@
    14.4      apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
    14.5      have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
    14.6      thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
    14.7 -      unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def
    14.8 +      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
    14.9        unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
   14.10    note lem3 = this[rule_format]
   14.11    have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
    15.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 18 17:42:35 2011 +0200
    15.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 18 13:36:58 2011 -0700
    15.3 @@ -401,14 +401,15 @@
    15.4  unfolding norm_vec_def
    15.5  by (rule member_le_setL2) simp_all
    15.6  
    15.7 -interpretation vec_nth: bounded_linear "\<lambda>x. x $ i"
    15.8 +lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
    15.9  apply default
   15.10  apply (rule vector_add_component)
   15.11  apply (rule vector_scaleR_component)
   15.12  apply (rule_tac x="1" in exI, simp add: norm_nth_le)
   15.13  done
   15.14  
   15.15 -declare vec_nth.isCont [simp]
   15.16 +lemmas isCont_vec_nth [simp] =
   15.17 +  bounded_linear.isCont [OF bounded_linear_vec_nth]
   15.18  
   15.19  instance vec :: (banach, finite) banach ..
   15.20  
    16.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 18 17:42:35 2011 +0200
    16.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 18 13:36:58 2011 -0700
    16.3 @@ -16,7 +16,7 @@
    16.4  
    16.5  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    16.6    scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
    16.7 -  scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
    16.8 +  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
    16.9  
   16.10  lemma real_arch_invD:
   16.11    "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
   16.12 @@ -1225,7 +1225,7 @@
   16.13  lemma has_integral_cmul:
   16.14    shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
   16.15    unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
   16.16 -  by(rule scaleR.bounded_linear_right)
   16.17 +  by(rule bounded_linear_scaleR_right)
   16.18  
   16.19  lemma has_integral_neg:
   16.20    shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
   16.21 @@ -2262,7 +2262,7 @@
   16.22    assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. norm(f x - g x) \<le> e"
   16.23    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})"
   16.24    apply(rule order_trans[OF _ rsum_bound[OF assms]]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
   16.25 -  unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR.diff_right by auto
   16.26 +  unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR_diff_right by auto
   16.27  
   16.28  lemma has_integral_bound: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
   16.29    assumes "0 \<le> B" "(f has_integral i) ({a..b})" "\<forall>x\<in>{a..b}. norm(f x) \<le> B"
   16.30 @@ -2287,7 +2287,7 @@
   16.31  lemma rsum_component_le: fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::euclidean_space"
   16.32    assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. (f x)$$i \<le> (g x)$$i"
   16.33    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"
   16.34 -  unfolding  euclidean_component.setsum apply(rule setsum_mono) apply safe
   16.35 +  unfolding  euclidean_component_setsum apply(rule setsum_mono) apply safe
   16.36  proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
   16.37    from this(3) guess u v apply-by(erule exE)+ note b=this
   16.38    show "(content b *\<^sub>R f a) $$ i \<le> (content b *\<^sub>R g a) $$ i" unfolding b
   16.39 @@ -2988,7 +2988,7 @@
   16.40        have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
   16.41          norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
   16.42          apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
   16.43 -        unfolding scaleR.diff_left by(auto simp add:algebra_simps)
   16.44 +        unfolding scaleR_diff_left by(auto simp add:algebra_simps)
   16.45        also have "... \<le> e * norm (u - x) + e * norm (v - x)"
   16.46          apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4
   16.47          apply(rule d(2)[of "x" "v",unfolded o_def])
   16.48 @@ -3123,7 +3123,7 @@
   16.49    assumes "continuous_on {a..b} f" "x \<in> {a..b}"
   16.50    shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
   16.51    unfolding has_vector_derivative_def has_derivative_within_alt
   16.52 -apply safe apply(rule scaleR.bounded_linear_left)
   16.53 +apply safe apply(rule bounded_linear_scaleR_left)
   16.54  proof- fix e::real assume e:"e>0"
   16.55    note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def]
   16.56    from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format]
   16.57 @@ -3223,8 +3223,8 @@
   16.58         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
   16.59          unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
   16.60          apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
   16.61 -      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]
   16.62 -        unfolding real_scaleR_def using assms(1) by auto finally have *:"?l = ?r" .
   16.63 +      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
   16.64 +        using assms(1) by auto finally have *:"?l = ?r" .
   16.65        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
   16.66          using assms(1) by(auto simp add:field_simps) qed qed qed
   16.67  
   16.68 @@ -3256,7 +3256,7 @@
   16.69  lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \<noteq> 0"
   16.70    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})"
   16.71    apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq[where 'a='a]
   16.72 -  unfolding scaleR_right_distrib euclidean_simps scaleR.scaleR_left[THEN sym]
   16.73 +  unfolding scaleR_right_distrib euclidean_simps scaleR_scaleR
   16.74    defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps)
   16.75    apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto
   16.76  
   16.77 @@ -3442,7 +3442,7 @@
   16.78      show ?case unfolding content_real[OF assms(1)] and *[of "\<lambda>x. x"] *[of f] setsum_subtractf[THEN sym] split_minus
   16.79        unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)]
   16.80      proof(rule norm_triangle_le,rule **) 
   16.81 -      case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst divide.setsum)
   16.82 +      case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib)
   16.83        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"
   16.84            "e * (interval_upperbound k -  interval_lowerbound k) / 2
   16.85            < norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))"
   16.86 @@ -4159,7 +4159,7 @@
   16.87        "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
   16.88        "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)" 
   16.89        unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg)
   16.90 -      apply safe unfolding real_scaleR_def mult.diff_right[THEN sym]
   16.91 +      apply safe unfolding real_scaleR_def right_diff_distrib[THEN sym]
   16.92        apply(rule_tac[!] mult_nonneg_nonneg)
   16.93      proof- fix a b assume ab:"(a,b) \<in> p1"
   16.94        show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
   16.95 @@ -4535,7 +4535,7 @@
   16.96           show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"])
   16.97             unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule norm_setsum)
   16.98             apply(rule setsum_mono) unfolding split_paired_all split_conv
   16.99 -           unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym]
  16.100 +           unfolding split_def setsum_left_distrib[THEN sym] scaleR_diff_right[THEN sym]
  16.101             unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
  16.102           proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto
  16.103             from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this
  16.104 @@ -5202,7 +5202,7 @@
  16.105  proof- have *:"\<And>x. ((\<chi>\<chi> i. abs(f x$$i))::'c::ordered_euclidean_space) = (setsum (\<lambda>i.
  16.106      (((\<lambda>y. (\<chi>\<chi> j. if j = i then y else 0)) o
  16.107      (((\<lambda>x. (norm((\<chi>\<chi> j. if j = i then x$$i else 0)::'c::ordered_euclidean_space))) o f))) x)) {..<DIM('c)})"
  16.108 -    unfolding euclidean_eq[where 'a='c] euclidean_component.setsum apply safe
  16.109 +    unfolding euclidean_eq[where 'a='c] euclidean_component_setsum apply safe
  16.110      unfolding euclidean_lambda_beta'
  16.111    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)) =
  16.112        (if i = xa then (f x $$ xa) * (f x $$ xa) else 0)" by auto
  16.113 @@ -5220,7 +5220,7 @@
  16.114      apply(rule absolutely_integrable_linear) unfolding o_def apply(rule absolutely_integrable_norm)
  16.115      apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear
  16.116      apply(rule_tac[!] linearI) unfolding euclidean_eq[where 'a='c]
  16.117 -    by(auto simp:euclidean_scaleR[where 'a=real,unfolded real_scaleR_def])
  16.118 +    by(auto simp:euclidean_component_scaleR[where 'a=real,unfolded real_scaleR_def])
  16.119  qed
  16.120  
  16.121  lemma absolutely_integrable_max: fixes f g::"'m::ordered_euclidean_space \<Rightarrow> 'n::ordered_euclidean_space"
  16.122 @@ -5266,7 +5266,7 @@
  16.123      proof- fix k and i assume "k\<in>d" and i:"i<DIM('m)"
  16.124        from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this
  16.125        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)
  16.126 -        unfolding euclidean_component.minus[THEN sym] defer apply(subst integral_neg[THEN sym])
  16.127 +        unfolding euclidean_component_minus[THEN sym] defer apply(subst integral_neg[THEN sym])
  16.128          defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg)
  16.129          using integrable_on_subinterval[OF assms(1),of a b]
  16.130            integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto
  16.131 @@ -5276,7 +5276,7 @@
  16.132          using integrable_on_subdivision[OF d assms(2)] by auto
  16.133        have "(\<Sum>i\<in>d. integral i (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j)
  16.134          = integral (\<Union>d) (\<lambda>x. (\<chi>\<chi> j. abs(f x$$j)) ::'m::ordered_euclidean_space) $$ j"
  16.135 -        unfolding euclidean_component.setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
  16.136 +        unfolding euclidean_component_setsum[THEN sym] integral_combine_division_topdown[OF * d] ..
  16.137        also have "... \<le> integral UNIV (\<lambda>x. (\<chi>\<chi> j. \<bar>f x $$ j\<bar>)::'m) $$ j"
  16.138          apply(rule integral_subset_component_le) using assms * by auto
  16.139        finally show ?case .
    17.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 17:42:35 2011 +0200
    17.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 13:36:58 2011 -0700
    17.3 @@ -198,8 +198,8 @@
    17.4  
    17.5  text{* Dot product in terms of the norm rather than conversely. *}
    17.6  
    17.7 -lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left 
    17.8 -inner.scaleR_left inner.scaleR_right
    17.9 +lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left 
   17.10 +inner_scaleR_left inner_scaleR_right
   17.11  
   17.12  lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
   17.13    unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
   17.14 @@ -1558,7 +1558,7 @@
   17.15    unfolding independent_eq_inj_on [OF basis_inj]
   17.16    apply clarify
   17.17    apply (drule_tac f="inner (basis a)" in arg_cong)
   17.18 -  apply (simp add: inner_right.setsum dot_basis)
   17.19 +  apply (simp add: inner_setsum_right dot_basis)
   17.20    done
   17.21  
   17.22  lemma dimensionI:
   17.23 @@ -1663,10 +1663,10 @@
   17.24      have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
   17.25      have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
   17.26        using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]
   17.27 -      unfolding euclidean_component.setsum by(auto intro: abs_le_D1)
   17.28 +      unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
   17.29      have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
   17.30        using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]
   17.31 -      unfolding euclidean_component.setsum euclidean_component.minus
   17.32 +      unfolding euclidean_component_setsum euclidean_component_minus
   17.33        by(auto simp add: setsum_negf intro: abs_le_D1)
   17.34      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"
   17.35        apply (subst thp)
   17.36 @@ -1756,7 +1756,7 @@
   17.37    have Kp: "?K > 0" by arith
   17.38      { assume C: "B < 0"
   17.39        have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
   17.40 -        by(auto intro!:exI[where x=0] simp add:euclidean_component.zero)
   17.41 +        by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
   17.42        hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
   17.43        with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
   17.44          by (simp add: mult_less_0_iff)
   17.45 @@ -2829,7 +2829,7 @@
   17.46      unfolding infnorm_def
   17.47      unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   17.48      unfolding infnorm_set_image ball_simps
   17.49 -    apply(subst (1) euclidean_eq) unfolding euclidean_component.zero
   17.50 +    apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
   17.51      by auto
   17.52    then show ?thesis using infnorm_pos_le[of x] by simp
   17.53  qed
   17.54 @@ -2881,7 +2881,7 @@
   17.55  lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \<bar>a\<bar> * infnorm x"
   17.56    apply (subst infnorm_def)
   17.57    unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   17.58 -  unfolding infnorm_set_image ball_simps euclidean_scaleR abs_mult
   17.59 +  unfolding infnorm_set_image ball_simps euclidean_component_scaleR abs_mult
   17.60    using component_le_infnorm[of x] by(auto intro: mult_mono) 
   17.61  
   17.62  lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
    18.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 17:42:35 2011 +0200
    18.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 13:36:58 2011 -0700
    18.3 @@ -14,7 +14,7 @@
    18.4  
    18.5  lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
    18.6    unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
    18.7 -  apply(auto simp add:power2_eq_square) unfolding euclidean_component.diff ..
    18.8 +  apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
    18.9  
   18.10  lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
   18.11    apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
   18.12 @@ -1912,7 +1912,7 @@
   18.13    fixes S :: "'a::real_normed_vector set"
   18.14    shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
   18.15    apply (rule bounded_linear_image, assumption)
   18.16 -  apply (rule scaleR.bounded_linear_right)
   18.17 +  apply (rule bounded_linear_scaleR_right)
   18.18    done
   18.19  
   18.20  lemma bounded_translation:
   18.21 @@ -3537,7 +3537,7 @@
   18.22  proof-
   18.23    { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
   18.24      hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
   18.25 -      using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
   18.26 +      using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
   18.27        unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
   18.28    }
   18.29    thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
   18.30 @@ -4365,7 +4365,7 @@
   18.31    assumes "compact s"  shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
   18.32  proof-
   18.33    let ?f = "\<lambda>x. scaleR c x"
   18.34 -  have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
   18.35 +  have *:"bounded_linear ?f" by (rule bounded_linear_scaleR_right)
   18.36    show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
   18.37      using linear_continuous_at[OF *] assms by auto
   18.38  qed
   18.39 @@ -4951,7 +4951,7 @@
   18.40          unfolding Lim_sequentially by(auto simp add: dist_norm)
   18.41        hence "(f ---> x) sequentially" unfolding f_def
   18.42          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]
   18.43 -        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  }
   18.44 +        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  }
   18.45      ultimately have "x \<in> closure {a<..<b}"
   18.46        using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto  }
   18.47    thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
   18.48 @@ -5571,7 +5571,7 @@
   18.49  subsection {* Some properties of a canonical subspace *}
   18.50  
   18.51  (** move **)
   18.52 -declare euclidean_component.zero[simp]  
   18.53 +declare euclidean_component_zero[simp]
   18.54  
   18.55  lemma subspace_substandard:
   18.56    "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
   18.57 @@ -6027,15 +6027,15 @@
   18.58  
   18.59  lemmas Lim_ident_at = LIM_ident
   18.60  lemmas Lim_const = tendsto_const
   18.61 -lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const]
   18.62 +lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
   18.63  lemmas Lim_neg = tendsto_minus
   18.64  lemmas Lim_add = tendsto_add
   18.65  lemmas Lim_sub = tendsto_diff
   18.66 -lemmas Lim_mul = scaleR.tendsto
   18.67 -lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
   18.68 +lemmas Lim_mul = tendsto_scaleR
   18.69 +lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
   18.70  lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
   18.71  lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
   18.72 -lemmas Lim_component = euclidean_component.tendsto
   18.73 +lemmas Lim_component = tendsto_euclidean_component
   18.74  lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
   18.75  
   18.76  end
    19.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Aug 18 17:42:35 2011 +0200
    19.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Aug 18 13:36:58 2011 -0700
    19.3 @@ -816,7 +816,7 @@
    19.4    proof cases
    19.5      assume "b \<noteq> 0"
    19.6      with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
    19.7 -      by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
    19.8 +      by (auto intro!: open_affinity simp: scaleR_add_right mem_def)
    19.9      hence "?S \<in> sets borel"
   19.10        unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
   19.11      moreover
    20.1 --- a/src/HOL/Probability/Independent_Family.thy	Thu Aug 18 17:42:35 2011 +0200
    20.2 +++ b/src/HOL/Probability/Independent_Family.thy	Thu Aug 18 13:36:58 2011 -0700
    20.3 @@ -563,7 +563,7 @@
    20.4      with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))"
    20.5        by simp
    20.6      moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))"
    20.7 -      by (intro mult_right.sums finite_measure_UNION F dis)
    20.8 +      by (intro sums_mult finite_measure_UNION F dis)
    20.9      ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)"
   20.10        by (auto dest!: sums_unique)
   20.11      with F show "(\<Union>i. F i) \<in> sets ?D"
    21.1 --- a/src/HOL/RealVector.thy	Thu Aug 18 17:42:35 2011 +0200
    21.2 +++ b/src/HOL/RealVector.thy	Thu Aug 18 13:36:58 2011 -0700
    21.3 @@ -62,24 +62,28 @@
    21.4    and scale_minus_left [simp]: "scale (- a) x = - (scale a x)"
    21.5    and scale_left_diff_distrib [algebra_simps]:
    21.6          "scale (a - b) x = scale a x - scale b x"
    21.7 +  and scale_setsum_left: "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)"
    21.8  proof -
    21.9    interpret s: additive "\<lambda>a. scale a x"
   21.10      proof qed (rule scale_left_distrib)
   21.11    show "scale 0 x = 0" by (rule s.zero)
   21.12    show "scale (- a) x = - (scale a x)" by (rule s.minus)
   21.13    show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
   21.14 +  show "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" by (rule s.setsum)
   21.15  qed
   21.16  
   21.17  lemma scale_zero_right [simp]: "scale a 0 = 0"
   21.18    and scale_minus_right [simp]: "scale a (- x) = - (scale a x)"
   21.19    and scale_right_diff_distrib [algebra_simps]:
   21.20          "scale a (x - y) = scale a x - scale a y"
   21.21 +  and scale_setsum_right: "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))"
   21.22  proof -
   21.23    interpret s: additive "\<lambda>x. scale a x"
   21.24      proof qed (rule scale_right_distrib)
   21.25    show "scale a 0 = 0" by (rule s.zero)
   21.26    show "scale a (- x) = - (scale a x)" by (rule s.minus)
   21.27    show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
   21.28 +  show "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" by (rule s.setsum)
   21.29  qed
   21.30  
   21.31  lemma scale_eq_0_iff [simp]:
   21.32 @@ -140,16 +144,16 @@
   21.33  end
   21.34  
   21.35  class real_vector = scaleR + ab_group_add +
   21.36 -  assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
   21.37 -  and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
   21.38 +  assumes scaleR_add_right: "scaleR a (x + y) = scaleR a x + scaleR a y"
   21.39 +  and scaleR_add_left: "scaleR (a + b) x = scaleR a x + scaleR b x"
   21.40    and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x"
   21.41    and scaleR_one: "scaleR 1 x = x"
   21.42  
   21.43  interpretation real_vector:
   21.44    vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
   21.45  apply unfold_locales
   21.46 -apply (rule scaleR_right_distrib)
   21.47 -apply (rule scaleR_left_distrib)
   21.48 +apply (rule scaleR_add_right)
   21.49 +apply (rule scaleR_add_left)
   21.50  apply (rule scaleR_scaleR)
   21.51  apply (rule scaleR_one)
   21.52  done
   21.53 @@ -159,16 +163,25 @@
   21.54  lemmas scaleR_left_commute = real_vector.scale_left_commute
   21.55  lemmas scaleR_zero_left = real_vector.scale_zero_left
   21.56  lemmas scaleR_minus_left = real_vector.scale_minus_left
   21.57 -lemmas scaleR_left_diff_distrib = real_vector.scale_left_diff_distrib
   21.58 +lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib
   21.59 +lemmas scaleR_setsum_left = real_vector.scale_setsum_left
   21.60  lemmas scaleR_zero_right = real_vector.scale_zero_right
   21.61  lemmas scaleR_minus_right = real_vector.scale_minus_right
   21.62 -lemmas scaleR_right_diff_distrib = real_vector.scale_right_diff_distrib
   21.63 +lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib
   21.64 +lemmas scaleR_setsum_right = real_vector.scale_setsum_right
   21.65  lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
   21.66  lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
   21.67  lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
   21.68  lemmas scaleR_cancel_left = real_vector.scale_cancel_left
   21.69  lemmas scaleR_cancel_right = real_vector.scale_cancel_right
   21.70  
   21.71 +text {* Legacy names *}
   21.72 +
   21.73 +lemmas scaleR_left_distrib = scaleR_add_left
   21.74 +lemmas scaleR_right_distrib = scaleR_add_right
   21.75 +lemmas scaleR_left_diff_distrib = scaleR_diff_left
   21.76 +lemmas scaleR_right_diff_distrib = scaleR_diff_right
   21.77 +
   21.78  lemma scaleR_minus1_left [simp]:
   21.79    fixes x :: "'a::real_vector"
   21.80    shows "scaleR (-1) x = - x"
   21.81 @@ -1059,8 +1072,8 @@
   21.82  
   21.83  end
   21.84  
   21.85 -interpretation mult:
   21.86 -  bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
   21.87 +lemma bounded_bilinear_mult:
   21.88 +  "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
   21.89  apply (rule bounded_bilinear.intro)
   21.90  apply (rule left_distrib)
   21.91  apply (rule right_distrib)
   21.92 @@ -1070,19 +1083,21 @@
   21.93  apply (simp add: norm_mult_ineq)
   21.94  done
   21.95  
   21.96 -interpretation mult_left:
   21.97 -  bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
   21.98 -by (rule mult.bounded_linear_left)
   21.99 +lemma bounded_linear_mult_left:
  21.100 +  "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
  21.101 +  using bounded_bilinear_mult
  21.102 +  by (rule bounded_bilinear.bounded_linear_left)
  21.103  
  21.104 -interpretation mult_right:
  21.105 -  bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
  21.106 -by (rule mult.bounded_linear_right)
  21.107 +lemma bounded_linear_mult_right:
  21.108 +  "bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)"
  21.109 +  using bounded_bilinear_mult
  21.110 +  by (rule bounded_bilinear.bounded_linear_right)
  21.111  
  21.112 -interpretation divide:
  21.113 -  bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
  21.114 -unfolding divide_inverse by (rule mult.bounded_linear_left)
  21.115 +lemma bounded_linear_divide:
  21.116 +  "bounded_linear (\<lambda>x::'a::real_normed_field. x / y)"
  21.117 +  unfolding divide_inverse by (rule bounded_linear_mult_left)
  21.118  
  21.119 -interpretation scaleR: bounded_bilinear "scaleR"
  21.120 +lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
  21.121  apply (rule bounded_bilinear.intro)
  21.122  apply (rule scaleR_left_distrib)
  21.123  apply (rule scaleR_right_distrib)
  21.124 @@ -1091,14 +1106,16 @@
  21.125  apply (rule_tac x="1" in exI, simp)
  21.126  done
  21.127  
  21.128 -interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
  21.129 -by (rule scaleR.bounded_linear_left)
  21.130 +lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
  21.131 +  using bounded_bilinear_scaleR
  21.132 +  by (rule bounded_bilinear.bounded_linear_left)
  21.133  
  21.134 -interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
  21.135 -by (rule scaleR.bounded_linear_right)
  21.136 +lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)"
  21.137 +  using bounded_bilinear_scaleR
  21.138 +  by (rule bounded_bilinear.bounded_linear_right)
  21.139  
  21.140 -interpretation of_real: bounded_linear "\<lambda>r. of_real r"
  21.141 -unfolding of_real_def by (rule scaleR.bounded_linear_left)
  21.142 +lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
  21.143 +  unfolding of_real_def by (rule bounded_linear_scaleR_left)
  21.144  
  21.145  subsection{* Hausdorff and other separation properties *}
  21.146  
    22.1 --- a/src/HOL/SEQ.thy	Thu Aug 18 17:42:35 2011 +0200
    22.2 +++ b/src/HOL/SEQ.thy	Thu Aug 18 13:36:58 2011 -0700
    22.3 @@ -377,7 +377,7 @@
    22.4  lemma LIMSEQ_mult:
    22.5    fixes a b :: "'a::real_normed_algebra"
    22.6    shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
    22.7 -by (rule mult.tendsto)
    22.8 +  by (rule tendsto_mult)
    22.9  
   22.10  lemma increasing_LIMSEQ:
   22.11    fixes f :: "nat \<Rightarrow> real"
    23.1 --- a/src/HOL/Series.thy	Thu Aug 18 17:42:35 2011 +0200
    23.2 +++ b/src/HOL/Series.thy	Thu Aug 18 13:36:58 2011 -0700
    23.3 @@ -211,50 +211,54 @@
    23.4    "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))"
    23.5  by (intro sums_unique sums summable_sums)
    23.6  
    23.7 +lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real]
    23.8 +lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
    23.9 +lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
   23.10 +
   23.11  lemma sums_mult:
   23.12    fixes c :: "'a::real_normed_algebra"
   23.13    shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
   23.14 -by (rule mult_right.sums)
   23.15 +  by (rule bounded_linear.sums [OF bounded_linear_mult_right])
   23.16  
   23.17  lemma summable_mult:
   23.18    fixes c :: "'a::real_normed_algebra"
   23.19    shows "summable f \<Longrightarrow> summable (%n. c * f n)"
   23.20 -by (rule mult_right.summable)
   23.21 +  by (rule bounded_linear.summable [OF bounded_linear_mult_right])
   23.22  
   23.23  lemma suminf_mult:
   23.24    fixes c :: "'a::real_normed_algebra"
   23.25    shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f"
   23.26 -by (rule mult_right.suminf [symmetric])
   23.27 +  by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric])
   23.28  
   23.29  lemma sums_mult2:
   23.30    fixes c :: "'a::real_normed_algebra"
   23.31    shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
   23.32 -by (rule mult_left.sums)
   23.33 +  by (rule bounded_linear.sums [OF bounded_linear_mult_left])
   23.34  
   23.35  lemma summable_mult2:
   23.36    fixes c :: "'a::real_normed_algebra"
   23.37    shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
   23.38 -by (rule mult_left.summable)
   23.39 +  by (rule bounded_linear.summable [OF bounded_linear_mult_left])
   23.40  
   23.41  lemma suminf_mult2:
   23.42    fixes c :: "'a::real_normed_algebra"
   23.43    shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
   23.44 -by (rule mult_left.suminf)
   23.45 +  by (rule bounded_linear.suminf [OF bounded_linear_mult_left])
   23.46  
   23.47  lemma sums_divide:
   23.48    fixes c :: "'a::real_normed_field"
   23.49    shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
   23.50 -by (rule divide.sums)
   23.51 +  by (rule bounded_linear.sums [OF bounded_linear_divide])
   23.52  
   23.53  lemma summable_divide:
   23.54    fixes c :: "'a::real_normed_field"
   23.55    shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
   23.56 -by (rule divide.summable)
   23.57 +  by (rule bounded_linear.summable [OF bounded_linear_divide])
   23.58  
   23.59  lemma suminf_divide:
   23.60    fixes c :: "'a::real_normed_field"
   23.61    shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
   23.62 -by (rule divide.suminf [symmetric])
   23.63 +  by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
   23.64  
   23.65  lemma sums_add:
   23.66    fixes a b :: "'a::real_normed_field"
   23.67 @@ -423,7 +427,7 @@
   23.68      by auto
   23.69    have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
   23.70      by simp
   23.71 -  thus ?thesis using divide.sums [OF 2, of 2]
   23.72 +  thus ?thesis using sums_divide [OF 2, of 2]
   23.73      by simp
   23.74  qed
   23.75  
    24.1 --- a/src/HOL/Transcendental.thy	Thu Aug 18 17:42:35 2011 +0200
    24.2 +++ b/src/HOL/Transcendental.thy	Thu Aug 18 13:36:58 2011 -0700
    24.3 @@ -971,7 +971,7 @@
    24.4  
    24.5  lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
    24.6  unfolding exp_def
    24.7 -apply (subst of_real.suminf)
    24.8 +apply (subst suminf_of_real)
    24.9  apply (rule summable_exp_generic)
   24.10  apply (simp add: scaleR_conv_of_real)
   24.11  done