src/ZF/ex/Ring.thy
changeset 29223 e09c53289830
parent 28952 15a4b2cf8c34
child 41524 4d2f9a1c24c7
     1.1 --- a/src/ZF/ex/Ring.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/ZF/ex/Ring.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4    minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
     1.5    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
     1.6  
     1.7 -locale abelian_monoid = struct G +
     1.8 +locale abelian_monoid = fixes G (structure)
     1.9    assumes a_comm_monoid: 
    1.10      "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
    1.11  
    1.12 @@ -57,7 +57,7 @@
    1.13    assumes a_comm_group: 
    1.14      "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
    1.15  
    1.16 -locale ring = abelian_group R + monoid R +
    1.17 +locale ring = abelian_group R + monoid R for R (structure) +
    1.18    assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
    1.19        \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
    1.20      and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
    1.21 @@ -262,7 +262,8 @@
    1.22  lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
    1.23  by (simp add: ring_hom_def)
    1.24  
    1.25 -locale ring_hom_cring = cring R + cring S + var h +
    1.26 +locale ring_hom_cring = R: cring R + S: cring S
    1.27 +  for R (structure) and S (structure) and h +
    1.28    assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
    1.29    notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
    1.30      and hom_mult [simp] = ring_hom_mult [OF homh]