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 \<in> carrier R" and S: "s \<in> carrier S"
   shows "eval R S h s (monom P r n) = h r \<otimes>\<^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 \<in> carrier P" and S: "s \<in> 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 (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 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 \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
   (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 \<in> 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 \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
     and mon0_closed: "monom P a 0 \<in> carrier P" 
     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> 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 \<in> 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 \<oplus>\<^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]: