src/HOL/Algebra/UnivPoly.thy
changeset 19931 fb32b43e7f80
parent 19783 82f365a14960
child 19984 29bb4659f80a
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -397,8 +397,8 @@
     1.4  *}
     1.5  
     1.6  interpretation UP_cring < cring P
     1.7 -  using UP_cring
     1.8 -  by - (erule cring.axioms)+
     1.9 +  by (intro_locales!)
    1.10 +    (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+
    1.11  
    1.12  
    1.13  subsection {* Polynomials form an Algebra *}
    1.14 @@ -441,8 +441,8 @@
    1.15      UP_smult_assoc1 UP_smult_assoc2)
    1.16  
    1.17  interpretation UP_cring < algebra R P
    1.18 -  using UP_algebra
    1.19 -  by - (erule algebra.axioms)+
    1.20 +  by (intro_locales!)
    1.21 +    (rule module.axioms algebra.axioms UP_algebra)+
    1.22  
    1.23  
    1.24  subsection {* Further lemmas involving monomials *}
    1.25 @@ -945,8 +945,7 @@
    1.26  *}
    1.27  
    1.28  interpretation UP_domain < "domain" P
    1.29 -  using UP_domain
    1.30 -  by (rule domain.axioms)
    1.31 +  by (intro_locales!) (rule domain.axioms UP_domain)+
    1.32  
    1.33  
    1.34  subsection {* Evaluation Homomorphism and Universal Property*}
    1.35 @@ -1148,9 +1147,15 @@
    1.36  text {* Interpretation of ring homomorphism lemmas. *}
    1.37  
    1.38  interpretation UP_univ_prop < ring_hom_cring P S Eval
    1.39 -  by (unfold Eval_def)
    1.40 -    (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems
    1.41 -      intro: ring_hom_cring_axioms.intro eval_ring_hom)
    1.42 +  apply (unfold Eval_def)
    1.43 +  apply (intro_locales!)
    1.44 +  apply (rule ring_hom_cring.axioms)
    1.45 +  apply (rule ring_hom_cring.intro)
    1.46 +  apply intro_locales
    1.47 +  apply (rule eval_ring_hom)
    1.48 +  apply rule
    1.49 +  done
    1.50 +
    1.51  
    1.52  text {* Further properties of the evaluation homomorphism. *}
    1.53  
    1.54 @@ -1220,8 +1225,8 @@
    1.55    assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
    1.56    shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
    1.57  proof -
    1.58 -  from S interpret UP_univ_prop [R S h P s _]
    1.59 -    by (auto intro!: UP_univ_prop_axioms.intro)
    1.60 +  interpret UP_univ_prop [R S h P s _]
    1.61 +    by (auto! intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
    1.62    from R
    1.63    show ?thesis by (rule Eval_monom)
    1.64  qed
    1.65 @@ -1271,7 +1276,7 @@
    1.66  proof (rule ring_hom_cring.intro)
    1.67    show "ring_hom_cring_axioms P S Phi"
    1.68    by (rule ring_hom_cring_axioms.intro) (rule Phi)
    1.69 -qed (auto intro: P.cring cring.axioms)
    1.70 +qed intro_locales
    1.71  
    1.72  theorem (in UP_pre_univ_prop) UP_universal_property:
    1.73    assumes S: "s \<in> carrier S"
    1.74 @@ -1291,9 +1296,9 @@
    1.75    assumes "cring R"
    1.76      and "cring S"
    1.77      and "h \<in> ring_hom R S"
    1.78 -  shows "UP_pre_univ_prop R S h "
    1.79 -  by (fast intro: UP_pre_univ_prop.intro ring_hom_cring_axioms.intro
    1.80 -    cring.axioms prems)
    1.81 +  shows "UP_pre_univ_prop R S h"
    1.82 +  by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
    1.83 +    ring_hom_cring_axioms.intro UP_cring.intro)
    1.84  
    1.85  constdefs
    1.86    INTEG :: "int ring"
    1.87 @@ -1315,8 +1320,10 @@
    1.88  *}
    1.89  
    1.90  interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
    1.91 +  apply simp
    1.92    using INTEG_id_eval
    1.93 -  by - (erule UP_pre_univ_prop.axioms)+
    1.94 +  apply simp
    1.95 +  done
    1.96  
    1.97  lemma INTEG_closed [intro, simp]:
    1.98    "z \<in> carrier INTEG"