# HG changeset patch # User huffman # Date 1180485686 -7200 # Node ID 56ee8105c002efb445da805b40fbea549a3521a6 # Parent 93f8cb025afdd38068e56f3e61decc5819a87ede simplify names of locale interpretations diff -r 93f8cb025afd -r 56ee8105c002 src/HOL/Hyperreal/Lim.thy --- 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 \ 'b::{recpower,real_normed_algebra}" @@ -519,7 +519,7 @@ "\isCont f a; isCont g a\ \ isCont (\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 \ isCont (\x. of_real (f x)) a" diff -r 93f8cb025afd -r 56ee8105c002 src/HOL/Hyperreal/SEQ.thy --- 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 (\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 \ Zseq (\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 \ Zseq (\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: "\X ----> a; Y ----> b\ \ (\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: "\(a::'a::division_ring) \ 0; b \ 0\ @@ -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 diff -r 93f8cb025afd -r 56ee8105c002 src/HOL/Hyperreal/Series.thy --- 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 \ (\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 \ 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 \ suminf (\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 \ (\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 \ summable (\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 \ suminf f * c = (\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 \ (\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 \ summable (\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 \ suminf (\n. f n / c) = suminf f / c" -by (rule bounded_linear_divide.suminf [symmetric]) +by (rule divide.suminf [symmetric]) lemma sums_add: "\X sums a; Y sums b\ \ (\n. X n + Y n) sums (a + b)" unfolding sums_def by (simp add: setsum_addf LIMSEQ_add) diff -r 93f8cb025afd -r 56ee8105c002 src/HOL/Hyperreal/Transcendental.thy --- 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 "\ = real (Suc n) *# (\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) = (\i=0..Suc n. S x i * S y (Suc n - i))" by (simp add: scaleR_cancel_left del: setsum_cl_ivl_Suc) diff -r 93f8cb025afd -r 56ee8105c002 src/HOL/Real/RealVector.thy --- 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 ["(\a. scaleR a x::'a::real_vector)"] -by (rule additive.intro, rule scaleR_left_distrib) +interpretation scaleR_left: additive ["(\a. scaleR a x::'a::real_vector)"] +by unfold_locales (rule scaleR_left_distrib) -interpretation additive_scaleR_right: - additive ["(\x. scaleR a x::'a::real_vector)"] -by (rule additive.intro, rule scaleR_right_distrib) +interpretation scaleR_right: additive ["(\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 \ 'a \ '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 ["(\x::'a::real_normed_algebra. x * y)"] -by (rule bounded_bilinear_mult.bounded_linear_left) - -interpretation bounded_linear_mult_right: - bounded_linear ["(\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 ["(\y::'a::real_normed_algebra. x * y)"] +by (rule mult.bounded_linear_right) + +interpretation divide: bounded_linear ["(\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 ["\r. of_real r"] -apply (unfold of_real_def) -apply (rule bounded_bilinear_scaleR.bounded_linear_left) -done +interpretation scaleR_left: bounded_linear ["\r. scaleR r x"] +by (rule scaleR.bounded_linear_left) + +interpretation scaleR_right: bounded_linear ["\x. scaleR r x"] +by (rule scaleR.bounded_linear_right) + +interpretation of_real: bounded_linear ["\r. of_real r"] +unfolding of_real_def by (rule scaleR.bounded_linear_left) end