Quelle  ring_with_one_def.pvs

%------------------------------------------------------------------------------
% Rings with one 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
%------------------------------------------------------------------------------

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

BEGIN

   IMPORTING ring_def[T,+,*,zero], monoid_def[T,*,one]

   S: VAR set[T]

   ring_with_one?(S):bool              = ring?(S) AND monoid?[T,*,one](S)
   finite_ring_with_one?(S): bool      = ring_with_one?(S) AND is_finite(S)
   commutative_ring_with_one?(S): bool = ring_with_one?(S) AND
                                         commutative?[(S)](*)
   finite_commutative_ring_with_one?(S): bool = finite_ring_with_one?(S) AND
                                                commutative?[(S)](*)

END ring_with_one_def