library Calculi/Algebra/Algebra

version 0.2
%author: S. Woelfl
%date: 16-06-2005

%(
    This library defines some basic concepts from the
    theory of relation algebras
)%


%left_assoc __cup__,__cap__,__cmps__
%prec {__cup__} < {__cmps__}
%prec {__cmps__} < {__cmpl__}


from Basic/Algebra_I get Monoid


logic CASL


spec SemiGroup =
     sort Elem
     op  __ * __: Elem * Elem -> Elem, assoc
end



spec InvolutedSemiGroup =
     SemiGroup
then
     op inv__:Elem -> Elem
     forall x,y:Elem
     . inv(x * y) = inv(y) * inv(x)
     . inv(inv(x)) = x
end


spec InvolutedMonoid =
     Monoid
and  InvolutedSemiGroup
then
     forall x:Elem
     . inv(e) = e
end