tuned monoid locales and prefix of sublocale interpretations

--- a/src/HOL/Groups.thy	Thu Mar 11 14:38:13 2010 +0100
+++ b/src/HOL/Groups.thy	Thu Mar 11 14:38:19 2010 +0100
@@ -68,13 +68,13 @@
 end
 
 locale monoid = semigroup +
-  fixes g :: 'a ("0")
-  assumes left_neutral [simp]: "0 * a = a"
-  assumes right_neutral [simp]: "a * 0 = a"
+  fixes z :: 'a ("1")
+  assumes left_neutral [simp]: "1 * a = a"
+  assumes right_neutral [simp]: "a * 1 = a"
 
 locale comm_monoid = abel_semigroup +
-  fixes g :: 'a ("0")
-  assumes comm_neutral: "a * 0 = a"
+  fixes z :: 'a ("1")
+  assumes comm_neutral: "a * 1 = a"
 
 sublocale comm_monoid < monoid proof
 qed (simp_all add: commute comm_neutral)
@@ -141,19 +141,19 @@
 class semigroup_add = plus +
   assumes add_assoc [algebra_simps]: "(a + b) + c = a + (b + c)"
 
-sublocale semigroup_add < plus!: semigroup plus proof
+sublocale semigroup_add < add!: semigroup plus proof
 qed (fact add_assoc)
 
 class ab_semigroup_add = semigroup_add +
   assumes add_commute [algebra_simps]: "a + b = b + a"
 
-sublocale ab_semigroup_add < plus!: abel_semigroup plus proof
+sublocale ab_semigroup_add < add!: abel_semigroup plus proof
 qed (fact add_commute)
 
 context ab_semigroup_add
 begin
 
-lemmas add_left_commute [algebra_simps] = plus.left_commute
+lemmas add_left_commute [algebra_simps] = add.left_commute
 
 theorems add_ac = add_assoc add_commute add_left_commute
 
@@ -164,19 +164,19 @@
 class semigroup_mult = times +
   assumes mult_assoc [algebra_simps]: "(a * b) * c = a * (b * c)"
 
-sublocale semigroup_mult < times!: semigroup times proof
+sublocale semigroup_mult < mult!: semigroup times proof
 qed (fact mult_assoc)
 
 class ab_semigroup_mult = semigroup_mult +
   assumes mult_commute [algebra_simps]: "a * b = b * a"
 
-sublocale ab_semigroup_mult < times!: abel_semigroup times proof
+sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
 qed (fact mult_commute)
 
 context ab_semigroup_mult
 begin
 
-lemmas mult_left_commute [algebra_simps] = times.left_commute
+lemmas mult_left_commute [algebra_simps] = mult.left_commute
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
@@ -188,7 +188,7 @@
   assumes add_0_left: "0 + a = a"
     and add_0_right: "a + 0 = a"
 
-sublocale monoid_add < zero!: monoid plus 0 proof
+sublocale monoid_add < add!: monoid plus 0 proof
 qed (fact add_0_left add_0_right)+
 
 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
@@ -197,17 +197,17 @@
 class comm_monoid_add = zero + ab_semigroup_add +
   assumes add_0: "0 + a = a"
 
-sublocale comm_monoid_add < zero!: comm_monoid plus 0 proof
+sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
 qed (insert add_0, simp add: ac_simps)
 
 subclass (in comm_monoid_add) monoid_add proof
-qed (fact zero.left_neutral zero.right_neutral)+
+qed (fact add.left_neutral add.right_neutral)+
 
 class monoid_mult = one + semigroup_mult +
   assumes mult_1_left: "1 * a  = a"
     and mult_1_right: "a * 1 = a"
 
-sublocale monoid_mult < one!: monoid times 1 proof
+sublocale monoid_mult < mult!: monoid times 1 proof
 qed (fact mult_1_left mult_1_right)+
 
 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
@@ -216,11 +216,11 @@
 class comm_monoid_mult = one + ab_semigroup_mult +
   assumes mult_1: "1 * a = a"
 
-sublocale comm_monoid_mult < one!: comm_monoid times 1 proof
+sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
 qed (insert mult_1, simp add: ac_simps)
 
 subclass (in comm_monoid_mult) monoid_mult proof
-qed (fact one.left_neutral one.right_neutral)+
+qed (fact mult.left_neutral mult.right_neutral)+
 
 class cancel_semigroup_add = semigroup_add +
   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"