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"