Quellcode-Bibliothek cyclic_monoid.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Cyclic monoids
%
%     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
%------------------------------------------------------------------------------

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

BEGIN

   ASSUMING IMPORTING cyclic_monoid_def[T,*,one]

       fullset_is_cyclic_monoid: ASSUMPTION cyclic_monoid?(fullset[T])

   ENDASSUMING

   IMPORTING monoid[T,*,one]

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

   M: VAR cyclic_monoid
   a: VAR T
   n: VAR nat

   cyclic_monoid_is: LEMMA cyclic_monoid?(M)

   cyclic_monoid_is_monoid: JUDGEMENT cyclic_monoid SUBTYPE_OF monoid

   cyclic_monoid_is_commutative_monoid:
                        JUDGEMENT cyclic_monoid SUBTYPE_OF commutative_monoid

END cyclic_monoid