1.1 --- a/src/HOL/Groups.thy	Wed Mar 10 16:53:27 2010 +0100
     1.2 +++ b/src/HOL/Groups.thy	Wed Mar 10 16:53:43 2010 +0100
     1.3 @@ -67,6 +67,18 @@
     1.4  
     1.5  end
     1.6  
     1.7 +locale monoid = semigroup +
     1.8 +  fixes g :: 'a ("0")
     1.9 +  assumes left_neutral [simp]: "0 * a = a"
    1.10 +  assumes right_neutral [simp]: "a * 0 = a"
    1.11 +
    1.12 +locale comm_monoid = abel_semigroup +
    1.13 +  fixes g :: 'a ("0")
    1.14 +  assumes comm_neutral: "a * 0 = a"
    1.15 +
    1.16 +sublocale comm_monoid < monoid proof
    1.17 +qed (simp_all add: commute comm_neutral)
    1.18 +
    1.19  
    1.20  subsection {* Generic operations *}
    1.21  
    1.22 @@ -173,36 +185,42 @@
    1.23  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.24  
    1.25  class monoid_add = zero + semigroup_add +
    1.26 -  assumes add_0_left [simp]: "0 + a = a"
    1.27 -    and add_0_right [simp]: "a + 0 = a"
    1.28 +  assumes add_0_left: "0 + a = a"
    1.29 +    and add_0_right: "a + 0 = a"
    1.30 +
    1.31 +sublocale monoid_add < zero!: monoid plus 0 proof
    1.32 +qed (fact add_0_left add_0_right)+
    1.33  
    1.34  lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
    1.35  by (rule eq_commute)
    1.36  
    1.37  class comm_monoid_add = zero + ab_semigroup_add +
    1.38    assumes add_0: "0 + a = a"
    1.39 -begin
    1.40  
    1.41 -subclass monoid_add
    1.42 -  proof qed (insert add_0, simp_all add: add_commute)
    1.43 +sublocale comm_monoid_add < zero!: comm_monoid plus 0 proof
    1.44 +qed (insert add_0, simp add: ac_simps)
    1.45  
    1.46 -end
    1.47 +subclass (in comm_monoid_add) monoid_add proof
    1.48 +qed (fact zero.left_neutral zero.right_neutral)+
    1.49  
    1.50  class monoid_mult = one + semigroup_mult +
    1.51 -  assumes mult_1_left [simp]: "1 * a  = a"
    1.52 -  assumes mult_1_right [simp]: "a * 1 = a"
    1.53 +  assumes mult_1_left: "1 * a  = a"
    1.54 +    and mult_1_right: "a * 1 = a"
    1.55 +
    1.56 +sublocale monoid_mult < one!: monoid times 1 proof
    1.57 +qed (fact mult_1_left mult_1_right)+
    1.58  
    1.59  lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
    1.60  by (rule eq_commute)
    1.61  
    1.62  class comm_monoid_mult = one + ab_semigroup_mult +
    1.63    assumes mult_1: "1 * a = a"
    1.64 -begin
    1.65  
    1.66 -subclass monoid_mult
    1.67 -  proof qed (insert mult_1, simp_all add: mult_commute)
    1.68 +sublocale comm_monoid_mult < one!: comm_monoid times 1 proof
    1.69 +qed (insert mult_1, simp add: ac_simps)
    1.70  
    1.71 -end
    1.72 +subclass (in comm_monoid_mult) monoid_mult proof
    1.73 +qed (fact one.left_neutral one.right_neutral)+
    1.74  
    1.75  class cancel_semigroup_add = semigroup_add +
    1.76    assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"