simplify names of locale interpretations
authorhuffman
Wed May 30 02:41:26 2007 +0200 (2007-05-30)
changeset 2312756ee8105c002
parent 23126 93f8cb025afd
child 23128 8e0abe0fa80f
simplify names of locale interpretations
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Real/RealVector.thy
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Wed May 30 01:53:38 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Wed May 30 02:41:26 2007 +0200
     1.3 @@ -371,17 +371,17 @@
     1.4  apply (erule LIM_right_zero)
     1.5  done
     1.6  
     1.7 -lemmas LIM_mult = bounded_bilinear_mult.LIM
     1.8 +lemmas LIM_mult = mult.LIM
     1.9  
    1.10 -lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero
    1.11 +lemmas LIM_mult_zero = mult.LIM_prod_zero
    1.12  
    1.13 -lemmas LIM_mult_left_zero = bounded_bilinear_mult.LIM_left_zero
    1.14 +lemmas LIM_mult_left_zero = mult.LIM_left_zero
    1.15  
    1.16 -lemmas LIM_mult_right_zero = bounded_bilinear_mult.LIM_right_zero
    1.17 +lemmas LIM_mult_right_zero = mult.LIM_right_zero
    1.18  
    1.19 -lemmas LIM_scaleR = bounded_bilinear_scaleR.LIM
    1.20 +lemmas LIM_scaleR = scaleR.LIM
    1.21  
    1.22 -lemmas LIM_of_real = bounded_linear_of_real.LIM
    1.23 +lemmas LIM_of_real = of_real.LIM
    1.24  
    1.25  lemma LIM_power:
    1.26    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
    1.27 @@ -519,7 +519,7 @@
    1.28    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
    1.29    unfolding isCont_def by (rule LIM)
    1.30  
    1.31 -lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont
    1.32 +lemmas isCont_scaleR = scaleR.isCont
    1.33  
    1.34  lemma isCont_of_real:
    1.35    "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)) a"
     2.1 --- a/src/HOL/Hyperreal/SEQ.thy	Wed May 30 01:53:38 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Wed May 30 02:41:26 2007 +0200
     2.3 @@ -197,7 +197,7 @@
     2.4      by (rule Zseq_imp_Zseq)
     2.5  qed
     2.6  
     2.7 -lemma (in bounded_bilinear) Zseq_prod:
     2.8 +lemma (in bounded_bilinear) Zseq:
     2.9    assumes X: "Zseq X"
    2.10    assumes Y: "Zseq Y"
    2.11    shows "Zseq (\<lambda>n. X n ** Y n)"
    2.12 @@ -277,17 +277,17 @@
    2.13    qed
    2.14  qed
    2.15  
    2.16 -lemma (in bounded_bilinear) Zseq_prod_left:
    2.17 +lemma (in bounded_bilinear) Zseq_left:
    2.18    "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
    2.19  by (rule bounded_linear_left [THEN bounded_linear.Zseq])
    2.20  
    2.21 -lemma (in bounded_bilinear) Zseq_prod_right:
    2.22 +lemma (in bounded_bilinear) Zseq_right:
    2.23    "Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)"
    2.24  by (rule bounded_linear_right [THEN bounded_linear.Zseq])
    2.25  
    2.26 -lemmas Zseq_mult = bounded_bilinear_mult.Zseq_prod
    2.27 -lemmas Zseq_mult_right = bounded_bilinear_mult.Zseq_prod_right
    2.28 -lemmas Zseq_mult_left = bounded_bilinear_mult.Zseq_prod_left
    2.29 +lemmas Zseq_mult = mult.Zseq
    2.30 +lemmas Zseq_mult_right = mult.Zseq_right
    2.31 +lemmas Zseq_mult_left = mult.Zseq_left
    2.32  
    2.33  
    2.34  subsection {* Limits of Sequences *}
    2.35 @@ -382,12 +382,12 @@
    2.36  lemma (in bounded_bilinear) LIMSEQ:
    2.37    "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b"
    2.38  by (simp only: LIMSEQ_Zseq_iff prod_diff_prod
    2.39 -               Zseq_add Zseq_prod Zseq_prod_left Zseq_prod_right)
    2.40 +               Zseq_add Zseq Zseq_left Zseq_right)
    2.41  
    2.42  lemma LIMSEQ_mult:
    2.43    fixes a b :: "'a::real_normed_algebra"
    2.44    shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
    2.45 -by (rule bounded_bilinear_mult.LIMSEQ)
    2.46 +by (rule mult.LIMSEQ)
    2.47  
    2.48  lemma inverse_diff_inverse:
    2.49    "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
    2.50 @@ -442,7 +442,7 @@
    2.51  apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero)
    2.52  apply (rule Zseq_minus)
    2.53  apply (rule Zseq_mult_left)
    2.54 -apply (rule bounded_bilinear_mult.Bseq_prod_Zseq)
    2.55 +apply (rule mult.Bseq_prod_Zseq)
    2.56  apply (erule (1) Bseq_inverse)
    2.57  apply (simp add: LIMSEQ_Zseq_iff)
    2.58  done
     3.1 --- a/src/HOL/Hyperreal/Series.thy	Wed May 30 01:53:38 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Series.thy	Wed May 30 02:41:26 2007 +0200
     3.3 @@ -171,47 +171,47 @@
     3.4  lemma sums_mult:
     3.5    fixes c :: "'a::real_normed_algebra"
     3.6    shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
     3.7 -by (rule bounded_linear_mult_right.sums)
     3.8 +by (rule mult_right.sums)
     3.9  
    3.10  lemma summable_mult:
    3.11    fixes c :: "'a::real_normed_algebra"
    3.12    shows "summable f \<Longrightarrow> summable (%n. c * f n)"
    3.13 -by (rule bounded_linear_mult_right.summable)
    3.14 +by (rule mult_right.summable)
    3.15  
    3.16  lemma suminf_mult:
    3.17    fixes c :: "'a::real_normed_algebra"
    3.18    shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f";
    3.19 -by (rule bounded_linear_mult_right.suminf [symmetric])
    3.20 +by (rule mult_right.suminf [symmetric])
    3.21  
    3.22  lemma sums_mult2:
    3.23    fixes c :: "'a::real_normed_algebra"
    3.24    shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
    3.25 -by (rule bounded_linear_mult_left.sums)
    3.26 +by (rule mult_left.sums)
    3.27  
    3.28  lemma summable_mult2:
    3.29    fixes c :: "'a::real_normed_algebra"
    3.30    shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
    3.31 -by (rule bounded_linear_mult_left.summable)
    3.32 +by (rule mult_left.summable)
    3.33  
    3.34  lemma suminf_mult2:
    3.35    fixes c :: "'a::real_normed_algebra"
    3.36    shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
    3.37 -by (rule bounded_linear_mult_left.suminf)
    3.38 +by (rule mult_left.suminf)
    3.39  
    3.40  lemma sums_divide:
    3.41    fixes c :: "'a::real_normed_field"
    3.42    shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
    3.43 -by (rule bounded_linear_divide.sums)
    3.44 +by (rule divide.sums)
    3.45  
    3.46  lemma summable_divide:
    3.47    fixes c :: "'a::real_normed_field"
    3.48    shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
    3.49 -by (rule bounded_linear_divide.summable)
    3.50 +by (rule divide.summable)
    3.51  
    3.52  lemma suminf_divide:
    3.53    fixes c :: "'a::real_normed_field"
    3.54    shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
    3.55 -by (rule bounded_linear_divide.suminf [symmetric])
    3.56 +by (rule divide.suminf [symmetric])
    3.57  
    3.58  lemma sums_add: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)"
    3.59  unfolding sums_def by (simp add: setsum_addf LIMSEQ_add)
     4.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed May 30 01:53:38 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed May 30 02:41:26 2007 +0200
     4.3 @@ -720,7 +720,7 @@
     4.4      by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
     4.5                real_of_nat_add [symmetric], simp)
     4.6    also have "\<dots> = real (Suc n) *# (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
     4.7 -    by (simp only: additive_scaleR_right.setsum)
     4.8 +    by (simp only: scaleR_right.setsum)
     4.9    finally show
    4.10      "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
    4.11      by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc)
     5.1 --- a/src/HOL/Real/RealVector.thy	Wed May 30 01:53:38 2007 +0200
     5.2 +++ b/src/HOL/Real/RealVector.thy	Wed May 30 02:41:26 2007 +0200
     5.3 @@ -91,25 +91,23 @@
     5.4    shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
     5.5  by (simp add: mult_commute)
     5.6  
     5.7 -interpretation additive_scaleR_left:
     5.8 -  additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
     5.9 -by (rule additive.intro, rule scaleR_left_distrib)
    5.10 +interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
    5.11 +by unfold_locales (rule scaleR_left_distrib)
    5.12  
    5.13 -interpretation additive_scaleR_right:
    5.14 -  additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
    5.15 -by (rule additive.intro, rule scaleR_right_distrib)
    5.16 +interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
    5.17 +by unfold_locales (rule scaleR_right_distrib)
    5.18  
    5.19 -lemmas scaleR_zero_left [simp] = additive_scaleR_left.zero
    5.20 +lemmas scaleR_zero_left [simp] = scaleR_left.zero
    5.21  
    5.22 -lemmas scaleR_zero_right [simp] = additive_scaleR_right.zero
    5.23 +lemmas scaleR_zero_right [simp] = scaleR_right.zero
    5.24  
    5.25 -lemmas scaleR_minus_left [simp] = additive_scaleR_left.minus
    5.26 +lemmas scaleR_minus_left [simp] = scaleR_left.minus
    5.27  
    5.28 -lemmas scaleR_minus_right [simp] = additive_scaleR_right.minus
    5.29 +lemmas scaleR_minus_right [simp] = scaleR_right.minus
    5.30  
    5.31 -lemmas scaleR_left_diff_distrib = additive_scaleR_left.diff
    5.32 +lemmas scaleR_left_diff_distrib = scaleR_left.diff
    5.33  
    5.34 -lemmas scaleR_right_diff_distrib = additive_scaleR_right.diff
    5.35 +lemmas scaleR_right_diff_distrib = scaleR_right.diff
    5.36  
    5.37  lemma scaleR_eq_0_iff [simp]:
    5.38    fixes x :: "'a::real_vector"
    5.39 @@ -737,7 +735,7 @@
    5.40    "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
    5.41  by (simp add: diff_left diff_right)
    5.42  
    5.43 -interpretation bounded_bilinear_mult:
    5.44 +interpretation mult:
    5.45    bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
    5.46  apply (rule bounded_bilinear.intro)
    5.47  apply (rule left_distrib)
    5.48 @@ -748,21 +746,19 @@
    5.49  apply (simp add: norm_mult_ineq)
    5.50  done
    5.51  
    5.52 -interpretation bounded_linear_mult_left:
    5.53 +interpretation mult_left:
    5.54    bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
    5.55 -by (rule bounded_bilinear_mult.bounded_linear_left)
    5.56 -
    5.57 -interpretation bounded_linear_mult_right:
    5.58 -  bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
    5.59 -by (rule bounded_bilinear_mult.bounded_linear_right)
    5.60 +by (rule mult.bounded_linear_left)
    5.61  
    5.62 -interpretation bounded_linear_divide:
    5.63 +interpretation mult_right:
    5.64 +  bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
    5.65 +by (rule mult.bounded_linear_right)
    5.66 +
    5.67 +interpretation divide:
    5.68    bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
    5.69 -unfolding divide_inverse
    5.70 -by (rule bounded_bilinear_mult.bounded_linear_left)
    5.71 +unfolding divide_inverse by (rule mult.bounded_linear_left)
    5.72  
    5.73 -interpretation bounded_bilinear_scaleR:
    5.74 -  bounded_bilinear ["scaleR"]
    5.75 +interpretation scaleR: bounded_bilinear ["scaleR"]
    5.76  apply (rule bounded_bilinear.intro)
    5.77  apply (rule scaleR_left_distrib)
    5.78  apply (rule scaleR_right_distrib)
    5.79 @@ -772,10 +768,13 @@
    5.80  apply (simp add: norm_scaleR)
    5.81  done
    5.82  
    5.83 -interpretation bounded_linear_of_real:
    5.84 -  bounded_linear ["\<lambda>r. of_real r"]
    5.85 -apply (unfold of_real_def)
    5.86 -apply (rule bounded_bilinear_scaleR.bounded_linear_left)
    5.87 -done
    5.88 +interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"]
    5.89 +by (rule scaleR.bounded_linear_left)
    5.90 +
    5.91 +interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"]
    5.92 +by (rule scaleR.bounded_linear_right)
    5.93 +
    5.94 +interpretation of_real: bounded_linear ["\<lambda>r. of_real r"]
    5.95 +unfolding of_real_def by (rule scaleR.bounded_linear_left)
    5.96  
    5.97  end