SSL monad_def.pvs

%------------------------------------------------------------------------------
% Monads definition file
%
%     Author: Rick Butler
%             David Lester, Manchester University & NIA
%
%     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
%------------------------------------------------------------------------------

monad_def[T:Type+,*:[T,T->T],one:T]: THEORY

BEGIN

  IMPORTING groupoid_def[T,*]

  S: VAR set[T]

  monad?(S): bool                    = groupoid?(S) AND
                                       member(one,S) AND
                                       identity?[(S)](*)(one)
  finite_monad?(S): bool             = monad?(S) AND is_finite(S)
  commutative_monad?(S): bool        = monad?(S) AND commutative?[(S)](*)
  finite_commutative_monad?(S): bool = finite_monad?(S) AND
                                       commutative?[(S)](*)

END monad_def