Quelle  semigroup.pvs

%------------------------------------------------------------------------------
% Semigroups
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%------------------------------------------------------------------------------

semigroup[T:Type+,*:[T,T->T]]: THEORY

BEGIN

   ASSUMING IMPORTING semigroup_def[T,*]

       fullset_is_semigroup: ASSUMPTION semigroup?(fullset[T])

   ENDASSUMING

   IMPORTING semigroup_def, groupoid[T,*]

   semigroup: TYPE+ = (semigroup?) CONTAINING fullset[T]

   x,y,z: VAR T

   associative:           LEMMA (x * y) * z = x * (y * z)

   semigroup_is_groupoid: JUDGEMENT semigroup SUBTYPE_OF groupoid


END semigroup