# HG changeset patch
# User haftmann
# Date 1201687067 -3600
# Node ID ad2756de580e0ae95f410e263c7ea46dc84b9ac6
# Parent  00c2c3525bef8efb3ac3a0d28507262a50b3c65b
idempotent semigroups

diff -r 00c2c3525bef -r ad2756de580e src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Jan 30 10:57:46 2008 +0100
+++ b/src/HOL/OrderedGroup.thy	Wed Jan 30 10:57:47 2008 +0100
@@ -58,6 +58,19 @@
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
+class ab_semigroup_idem_mult = ab_semigroup_mult +
+  assumes mult_idem: "x * x = x"
+begin
+
+lemma mult_left_idem: "x * (x * y) = x * y"
+  unfolding mult_assoc [symmetric, of x] mult_idem ..
+
+lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem
+
+end
+
+lemmas mult_ac_idem = mult_ac mult_idem mult_left_idem
+
 class monoid_add = zero + semigroup_add +
   assumes add_0_left [simp]: "0 + a = a"
     and add_0_right [simp]: "a + 0 = a"