src/HOL/Algebra/Ring.thy
changeset 29237 e90d9d51106b
parent 28823 dcbef866c9e2
child 35054 a5db9779b026
     1.1 --- a/src/HOL/Algebra/Ring.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5    Title:     The algebraic hierarchy of rings
     1.6 -  Id:        $Id$
     1.7    Author:    Clemens Ballarin, started 9 December 1996
     1.8    Copyright: Clemens Ballarin
     1.9  *)
    1.10 @@ -187,7 +186,7 @@
    1.11    assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.12    shows "abelian_group G"
    1.13  proof -
    1.14 -  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
    1.15 +  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.16      by (rule cg)
    1.17    show "abelian_group G" ..
    1.18  qed
    1.19 @@ -360,7 +359,7 @@
    1.20  
    1.21  subsection {* Rings: Basic Definitions *}
    1.22  
    1.23 -locale ring = abelian_group R + monoid R +
    1.24 +locale ring = abelian_group R + monoid R for R (structure) +
    1.25    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.26        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
    1.27      and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
    1.28 @@ -585,8 +584,8 @@
    1.29    assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
    1.30    shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
    1.31  proof -
    1.32 -  interpret ring [R] by fact
    1.33 -  interpret cring [S] by fact
    1.34 +  interpret ring R by fact
    1.35 +  interpret cring S by fact
    1.36  ML_val {* Algebra.print_structures @{context} *}
    1.37    from RS show ?thesis by algebra
    1.38  qed
    1.39 @@ -597,7 +596,7 @@
    1.40    assumes R: "a \<in> carrier R" "b \<in> carrier R"
    1.41    shows "a \<ominus> (a \<ominus> b) = b"
    1.42  proof -
    1.43 -  interpret ring [R] by fact
    1.44 +  interpret ring R by fact
    1.45    from R show ?thesis by algebra
    1.46  qed
    1.47  
    1.48 @@ -771,7 +770,8 @@
    1.49    shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
    1.50    by (simp add: ring_hom_def)
    1.51  
    1.52 -locale ring_hom_cring = cring R + cring S +
    1.53 +locale ring_hom_cring = R: cring R + S: cring S
    1.54 +    for R (structure) and S (structure) +
    1.55    fixes h
    1.56    assumes homh [simp, intro]: "h \<in> ring_hom R S"
    1.57    notes hom_closed [simp, intro] = ring_hom_closed [OF homh]