diff -r 51526dd8da8e -r e90d9d51106b src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Tue Dec 16 15:09:37 2008 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Tue Dec 16 21:10:53 2008 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Algebra/UnivPoly.thy - Id: \$Id\$ Author: Clemens Ballarin, started 9 December 1996 Copyright: Clemens Ballarin @@ -180,12 +179,12 @@ locale UP_cring = UP + cring R -interpretation UP_cring < UP_ring +sublocale UP_cring < UP_ring by (rule P_def) intro_locales locale UP_domain = UP + "domain" R -interpretation UP_domain < UP_cring +sublocale UP_domain < UP_cring by (rule P_def) intro_locales context UP @@ -458,8 +457,8 @@ end -interpretation UP_ring < ring P using UP_ring . -interpretation UP_cring < cring P using UP_cring . +sublocale UP_ring < ring P using UP_ring . +sublocale UP_cring < cring P using UP_cring . subsection {* Polynomials Form an Algebra *} @@ -508,7 +507,7 @@ "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr UP_smult_assoc1 UP_smult_assoc2) -interpretation UP_cring < algebra R P using UP_algebra . +sublocale UP_cring < algebra R P using UP_algebra . subsection {* Further Lemmas Involving Monomials *} @@ -1085,7 +1084,7 @@ Interpretation of theorems from @{term domain}. *} -interpretation UP_domain < "domain" P +sublocale UP_domain < "domain" P by intro_locales (rule domain.axioms UP_domain)+ @@ -1350,7 +1349,7 @@ text {* Interpretation of ring homomorphism lemmas. *} -interpretation UP_univ_prop < ring_hom_cring P S Eval +sublocale UP_univ_prop < ring_hom_cring P S Eval apply (unfold Eval_def) apply intro_locales apply (rule ring_hom_cring.axioms) @@ -1391,7 +1390,7 @@ assumes R: "r \ carrier R" and S: "s \ carrier S" shows "eval R S h s (monom P r n) = h r \\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n" proof - - interpret UP_univ_prop [R S h P s _] + interpret UP_univ_prop R S h P s "eval R S h s" using UP_pre_univ_prop_axioms P_def R S by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro) from R @@ -1428,8 +1427,8 @@ and P: "p \ carrier P" and S: "s \ carrier S" shows "Phi p = Psi p" proof - - interpret ring_hom_cring [P S Phi] by fact - interpret ring_hom_cring [P S Psi] by fact + interpret ring_hom_cring P S Phi by fact + interpret ring_hom_cring P S Psi by fact have "Phi p = Phi (\\<^bsub>P \<^esub>i \ {..deg R p}. monom P (coeff P p i) 0 \\<^bsub>P\<^esub> monom P \ 1 (^)\<^bsub>P\<^esub> i)" by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult) @@ -1772,9 +1771,9 @@ shows "eval R R id a (monom P \\<^bsub>R\<^esub> 1 \\<^bsub>P\<^esub> monom P a 0) = \" (is "eval R R id a ?g = _") proof - - interpret UP_pre_univ_prop [R R id P] proof qed simp + interpret UP_pre_univ_prop R R id P proof qed simp have eval_ring_hom: "eval R R id a \ ring_hom P R" using eval_ring_hom [OF a] by simp - interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom) + interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom) have mon1_closed: "monom P \\<^bsub>R\<^esub> 1 \ carrier P" and mon0_closed: "monom P a 0 \ carrier P" and min_mon0_closed: "\\<^bsub>P\<^esub> monom P a 0 \ carrier P" @@ -1819,7 +1818,7 @@ and deg_r_0: "deg R r = 0" shows "r = monom P (eval R R id a f) 0" proof - - interpret UP_pre_univ_prop [R R id P] proof qed simp + interpret UP_pre_univ_prop R R id P proof qed simp have eval_ring_hom: "eval R R id a \ ring_hom P R" using eval_ring_hom [OF a] by simp have "eval R R id a f = eval R R id a ?gq \\<^bsub>R\<^esub> eval R R id a r" @@ -1885,7 +1884,7 @@ "UP INTEG"} globally. *} -interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] +interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id using INTEG_id_eval by simp_all lemma INTEG_closed [intro, simp]: