--- a/src/HOL/Hyperreal/Lim.thy Wed May 30 01:53:38 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed May 30 02:41:26 2007 +0200
@@ -371,17 +371,17 @@
apply (erule LIM_right_zero)
done
-lemmas LIM_mult = bounded_bilinear_mult.LIM
+lemmas LIM_mult = mult.LIM
-lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero
+lemmas LIM_mult_zero = mult.LIM_prod_zero
-lemmas LIM_mult_left_zero = bounded_bilinear_mult.LIM_left_zero
+lemmas LIM_mult_left_zero = mult.LIM_left_zero
-lemmas LIM_mult_right_zero = bounded_bilinear_mult.LIM_right_zero
+lemmas LIM_mult_right_zero = mult.LIM_right_zero
-lemmas LIM_scaleR = bounded_bilinear_scaleR.LIM
+lemmas LIM_scaleR = scaleR.LIM
-lemmas LIM_of_real = bounded_linear_of_real.LIM
+lemmas LIM_of_real = of_real.LIM
lemma LIM_power:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
@@ -519,7 +519,7 @@
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
unfolding isCont_def by (rule LIM)
-lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont
+lemmas isCont_scaleR = scaleR.isCont
lemma isCont_of_real:
"isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)) a"
--- a/src/HOL/Hyperreal/SEQ.thy Wed May 30 01:53:38 2007 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Wed May 30 02:41:26 2007 +0200
@@ -197,7 +197,7 @@
by (rule Zseq_imp_Zseq)
qed
-lemma (in bounded_bilinear) Zseq_prod:
+lemma (in bounded_bilinear) Zseq:
assumes X: "Zseq X"
assumes Y: "Zseq Y"
shows "Zseq (\<lambda>n. X n ** Y n)"
@@ -277,17 +277,17 @@
qed
qed
-lemma (in bounded_bilinear) Zseq_prod_left:
+lemma (in bounded_bilinear) Zseq_left:
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
by (rule bounded_linear_left [THEN bounded_linear.Zseq])
-lemma (in bounded_bilinear) Zseq_prod_right:
+lemma (in bounded_bilinear) Zseq_right:
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)"
by (rule bounded_linear_right [THEN bounded_linear.Zseq])
-lemmas Zseq_mult = bounded_bilinear_mult.Zseq_prod
-lemmas Zseq_mult_right = bounded_bilinear_mult.Zseq_prod_right
-lemmas Zseq_mult_left = bounded_bilinear_mult.Zseq_prod_left
+lemmas Zseq_mult = mult.Zseq
+lemmas Zseq_mult_right = mult.Zseq_right
+lemmas Zseq_mult_left = mult.Zseq_left
subsection {* Limits of Sequences *}
@@ -382,12 +382,12 @@
lemma (in bounded_bilinear) LIMSEQ:
"\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b"
by (simp only: LIMSEQ_Zseq_iff prod_diff_prod
- Zseq_add Zseq_prod Zseq_prod_left Zseq_prod_right)
+ Zseq_add Zseq Zseq_left Zseq_right)
lemma LIMSEQ_mult:
fixes a b :: "'a::real_normed_algebra"
shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
-by (rule bounded_bilinear_mult.LIMSEQ)
+by (rule mult.LIMSEQ)
lemma inverse_diff_inverse:
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
@@ -442,7 +442,7 @@
apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero)
apply (rule Zseq_minus)
apply (rule Zseq_mult_left)
-apply (rule bounded_bilinear_mult.Bseq_prod_Zseq)
+apply (rule mult.Bseq_prod_Zseq)
apply (erule (1) Bseq_inverse)
apply (simp add: LIMSEQ_Zseq_iff)
done
--- a/src/HOL/Hyperreal/Series.thy Wed May 30 01:53:38 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy Wed May 30 02:41:26 2007 +0200
@@ -171,47 +171,47 @@
lemma sums_mult:
fixes c :: "'a::real_normed_algebra"
shows "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)"
-by (rule bounded_linear_mult_right.sums)
+by (rule mult_right.sums)
lemma summable_mult:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> summable (%n. c * f n)"
-by (rule bounded_linear_mult_right.summable)
+by (rule mult_right.summable)
lemma suminf_mult:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f";
-by (rule bounded_linear_mult_right.suminf [symmetric])
+by (rule mult_right.suminf [symmetric])
lemma sums_mult2:
fixes c :: "'a::real_normed_algebra"
shows "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)"
-by (rule bounded_linear_mult_left.sums)
+by (rule mult_left.sums)
lemma summable_mult2:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)"
-by (rule bounded_linear_mult_left.summable)
+by (rule mult_left.summable)
lemma suminf_mult2:
fixes c :: "'a::real_normed_algebra"
shows "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)"
-by (rule bounded_linear_mult_left.suminf)
+by (rule mult_left.suminf)
lemma sums_divide:
fixes c :: "'a::real_normed_field"
shows "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)"
-by (rule bounded_linear_divide.sums)
+by (rule divide.sums)
lemma summable_divide:
fixes c :: "'a::real_normed_field"
shows "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)"
-by (rule bounded_linear_divide.summable)
+by (rule divide.summable)
lemma suminf_divide:
fixes c :: "'a::real_normed_field"
shows "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
-by (rule bounded_linear_divide.suminf [symmetric])
+by (rule divide.suminf [symmetric])
lemma sums_add: "\<lbrakk>X sums a; Y sums b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) sums (a + b)"
unfolding sums_def by (simp add: setsum_addf LIMSEQ_add)
--- a/src/HOL/Hyperreal/Transcendental.thy Wed May 30 01:53:38 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed May 30 02:41:26 2007 +0200
@@ -720,7 +720,7 @@
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
real_of_nat_add [symmetric], simp)
also have "\<dots> = real (Suc n) *# (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
- by (simp only: additive_scaleR_right.setsum)
+ by (simp only: scaleR_right.setsum)
finally show
"S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc)
--- a/src/HOL/Real/RealVector.thy Wed May 30 01:53:38 2007 +0200
+++ b/src/HOL/Real/RealVector.thy Wed May 30 02:41:26 2007 +0200
@@ -91,25 +91,23 @@
shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
by (simp add: mult_commute)
-interpretation additive_scaleR_left:
- additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
-by (rule additive.intro, rule scaleR_left_distrib)
+interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
+by unfold_locales (rule scaleR_left_distrib)
-interpretation additive_scaleR_right:
- additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
-by (rule additive.intro, rule scaleR_right_distrib)
+interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
+by unfold_locales (rule scaleR_right_distrib)
-lemmas scaleR_zero_left [simp] = additive_scaleR_left.zero
+lemmas scaleR_zero_left [simp] = scaleR_left.zero
-lemmas scaleR_zero_right [simp] = additive_scaleR_right.zero
+lemmas scaleR_zero_right [simp] = scaleR_right.zero
-lemmas scaleR_minus_left [simp] = additive_scaleR_left.minus
+lemmas scaleR_minus_left [simp] = scaleR_left.minus
-lemmas scaleR_minus_right [simp] = additive_scaleR_right.minus
+lemmas scaleR_minus_right [simp] = scaleR_right.minus
-lemmas scaleR_left_diff_distrib = additive_scaleR_left.diff
+lemmas scaleR_left_diff_distrib = scaleR_left.diff
-lemmas scaleR_right_diff_distrib = additive_scaleR_right.diff
+lemmas scaleR_right_diff_distrib = scaleR_right.diff
lemma scaleR_eq_0_iff [simp]:
fixes x :: "'a::real_vector"
@@ -737,7 +735,7 @@
"(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
by (simp add: diff_left diff_right)
-interpretation bounded_bilinear_mult:
+interpretation mult:
bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
apply (rule bounded_bilinear.intro)
apply (rule left_distrib)
@@ -748,21 +746,19 @@
apply (simp add: norm_mult_ineq)
done
-interpretation bounded_linear_mult_left:
+interpretation mult_left:
bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
-by (rule bounded_bilinear_mult.bounded_linear_left)
-
-interpretation bounded_linear_mult_right:
- bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
-by (rule bounded_bilinear_mult.bounded_linear_right)
+by (rule mult.bounded_linear_left)
-interpretation bounded_linear_divide:
+interpretation mult_right:
+ bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
+by (rule mult.bounded_linear_right)
+
+interpretation divide:
bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
-unfolding divide_inverse
-by (rule bounded_bilinear_mult.bounded_linear_left)
+unfolding divide_inverse by (rule mult.bounded_linear_left)
-interpretation bounded_bilinear_scaleR:
- bounded_bilinear ["scaleR"]
+interpretation scaleR: bounded_bilinear ["scaleR"]
apply (rule bounded_bilinear.intro)
apply (rule scaleR_left_distrib)
apply (rule scaleR_right_distrib)
@@ -772,10 +768,13 @@
apply (simp add: norm_scaleR)
done
-interpretation bounded_linear_of_real:
- bounded_linear ["\<lambda>r. of_real r"]
-apply (unfold of_real_def)
-apply (rule bounded_bilinear_scaleR.bounded_linear_left)
-done
+interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"]
+by (rule scaleR.bounded_linear_left)
+
+interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"]
+by (rule scaleR.bounded_linear_right)
+
+interpretation of_real: bounded_linear ["\<lambda>r. of_real r"]
+unfolding of_real_def by (rule scaleR.bounded_linear_left)
end