src/HOL/OrderedGroup.thy
changeset 26015 ad2756de580e
parent 25762 c03e9d04b3e4
child 26071 046fe7ddfc4b
     1.1 --- a/src/HOL/OrderedGroup.thy	Wed Jan 30 10:57:46 2008 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Wed Jan 30 10:57:47 2008 +0100
     1.3 @@ -58,6 +58,19 @@
     1.4  
     1.5  theorems mult_ac = mult_assoc mult_commute mult_left_commute
     1.6  
     1.7 +class ab_semigroup_idem_mult = ab_semigroup_mult +
     1.8 +  assumes mult_idem: "x * x = x"
     1.9 +begin
    1.10 +
    1.11 +lemma mult_left_idem: "x * (x * y) = x * y"
    1.12 +  unfolding mult_assoc [symmetric, of x] mult_idem ..
    1.13 +
    1.14 +lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem
    1.15 +
    1.16 +end
    1.17 +
    1.18 +lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem
    1.19 +
    1.20  class monoid_add = zero + semigroup_add +
    1.21    assumes add_0_left [simp]: "0 + a = a"
    1.22      and add_0_right [simp]: "a + 0 = a"