Quelle  commutative_semigroup.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Commutative 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
%------------------------------------------------------------------------------

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

BEGIN

   ASSUMING IMPORTING semigroup_def[T,*]

       fullset_is_commutative_semigroup:
                                  ASSUMPTION commutative_semigroup?(fullset[T])

   ENDASSUMING

   IMPORTING semigroup_def, commutative_groupoid[T,*], semigroup[T,*]

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

   commutative_semigroup_is_semigroup:
               JUDGEMENT commutative_semigroup SUBTYPE_OF semigroup
   commutative_semigroup_is_commutative_groupoid:
               JUDGEMENT commutative_semigroup SUBTYPE_OF commutative_groupoid

END commutative_semigroup