src/HOL/Algebra/UnivPoly.thy
changeset 29237 e90d9d51106b
parent 28823 dcbef866c9e2
child 29240 bb81c3709fb6
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5    Title:     HOL/Algebra/UnivPoly.thy
     1.6 -  Id:        $Id$
     1.7    Author:    Clemens Ballarin, started 9 December 1996
     1.8    Copyright: Clemens Ballarin
     1.9  
    1.10 @@ -180,12 +179,12 @@
    1.11  
    1.12  locale UP_cring = UP + cring R
    1.13  
    1.14 -interpretation UP_cring < UP_ring
    1.15 +sublocale UP_cring < UP_ring
    1.16    by (rule P_def) intro_locales
    1.17  
    1.18  locale UP_domain = UP + "domain" R
    1.19  
    1.20 -interpretation UP_domain < UP_cring
    1.21 +sublocale UP_domain < UP_cring
    1.22    by (rule P_def) intro_locales
    1.23  
    1.24  context UP
    1.25 @@ -458,8 +457,8 @@
    1.26  
    1.27  end
    1.28  
    1.29 -interpretation UP_ring < ring P using UP_ring .
    1.30 -interpretation UP_cring < cring P using UP_cring .
    1.31 +sublocale UP_ring < ring P using UP_ring .
    1.32 +sublocale UP_cring < cring P using UP_cring .
    1.33  
    1.34  
    1.35  subsection {* Polynomials Form an Algebra *}
    1.36 @@ -508,7 +507,7 @@
    1.37    "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
    1.38      UP_smult_assoc1 UP_smult_assoc2)
    1.39  
    1.40 -interpretation UP_cring < algebra R P using UP_algebra .
    1.41 +sublocale UP_cring < algebra R P using UP_algebra .
    1.42  
    1.43  
    1.44  subsection {* Further Lemmas Involving Monomials *}
    1.45 @@ -1085,7 +1084,7 @@
    1.46    Interpretation of theorems from @{term domain}.
    1.47  *}
    1.48  
    1.49 -interpretation UP_domain < "domain" P
    1.50 +sublocale UP_domain < "domain" P
    1.51    by intro_locales (rule domain.axioms UP_domain)+
    1.52  
    1.53  
    1.54 @@ -1350,7 +1349,7 @@
    1.55  
    1.56  text {* Interpretation of ring homomorphism lemmas. *}
    1.57  
    1.58 -interpretation UP_univ_prop < ring_hom_cring P S Eval
    1.59 +sublocale UP_univ_prop < ring_hom_cring P S Eval
    1.60    apply (unfold Eval_def)
    1.61    apply intro_locales
    1.62    apply (rule ring_hom_cring.axioms)
    1.63 @@ -1391,7 +1390,7 @@
    1.64    assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
    1.65    shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
    1.66  proof -
    1.67 -  interpret UP_univ_prop [R S h P s _]
    1.68 +  interpret UP_univ_prop R S h P s "eval R S h s"
    1.69      using UP_pre_univ_prop_axioms P_def R S
    1.70      by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
    1.71    from R
    1.72 @@ -1428,8 +1427,8 @@
    1.73      and P: "p \<in> carrier P" and S: "s \<in> carrier S"
    1.74    shows "Phi p = Psi p"
    1.75  proof -
    1.76 -  interpret ring_hom_cring [P S Phi] by fact
    1.77 -  interpret ring_hom_cring [P S Psi] by fact
    1.78 +  interpret ring_hom_cring P S Phi by fact
    1.79 +  interpret ring_hom_cring P S Psi by fact
    1.80    have "Phi p =
    1.81        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)"
    1.82      by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
    1.83 @@ -1772,9 +1771,9 @@
    1.84    shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
    1.85    (is "eval R R id a ?g = _")
    1.86  proof -
    1.87 -  interpret UP_pre_univ_prop [R R id P] proof qed simp
    1.88 +  interpret UP_pre_univ_prop R R id P proof qed simp
    1.89    have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
    1.90 -  interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom)
    1.91 +  interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
    1.92    have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
    1.93      and mon0_closed: "monom P a 0 \<in> carrier P" 
    1.94      and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
    1.95 @@ -1819,7 +1818,7 @@
    1.96      and deg_r_0: "deg R r = 0"
    1.97      shows "r = monom P (eval R R id a f) 0"
    1.98  proof -
    1.99 -  interpret UP_pre_univ_prop [R R id P] proof qed simp
   1.100 +  interpret UP_pre_univ_prop R R id P proof qed simp
   1.101    have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
   1.102      using eval_ring_hom [OF a] by simp
   1.103    have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
   1.104 @@ -1885,7 +1884,7 @@
   1.105    "UP INTEG"} globally.
   1.106  *}
   1.107  
   1.108 -interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
   1.109 +interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
   1.110    using INTEG_id_eval by simp_all
   1.111  
   1.112  lemma INTEG_closed [intro, simp]: