%------------------------------------------------------------------------------
% Monoids definition file
%
%     Author: Rick Butler,  NASA Langley
%             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
%------------------------------------------------------------------------------

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

BEGIN

   IMPORTING monad_def[T,*,one]

   S: VAR set[T]
   a: VAR T
   n,m: VAR nat

   power(a,n):RECURSIVE T = IF n=0 THEN one ELSE a*power(a,n-1) ENDIF MEASURE n


   generated_set(a):set[T] = {t: T | EXISTS n: t = power(a,n)}

   generated_set_lem   : LEMMA generated_set(a)(power(a,n))

   monoid?(S): bool                    = monad?(S)  AND associative?[(S)](*)
   finite_monoid?(S): bool             = monoid?(S) AND is_finite(S)
   commutative_monoid?(S): bool        = monoid?(S) AND commutative?[(S)](*)
   finite_commutative_monoid?(S): bool = finite_monoid?(S) AND
                                         commutative?[(S)](*)

   infinite_order?(a):bool = (FORALL (n:posnat): power(a,n) /= one)
   finite_order?(a)  :bool = NOT infinite_order?(a)

END monoid_def