Quelle  ring_def.pvs

%------------------------------------------------------------------------------
% Rings 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_def[T:Type+,+,*:[T,T->T],zero:T]: THEORY

BEGIN

  IMPORTING semigroup_def, group_def, operator_defs_more

  S: VAR set[T]

  ring?(S): bool = abelian_group?[T,+,zero](S)  AND
                   semigroup?[T,*](S)           AND
                   left_distributive?[(S)](*,+) AND
                   right_distributive?[(S)](*,+)

  finite_ring?(S): bool              = ring?(S) AND is_finite(S)
  commutative_ring?(S): bool         = ring?(S) AND commutative?[(S)](*)
  finite_commutative_ring?(S): bool  = finite_ring?(S) AND commutative?[(S)](*)

  subring?(S:set[T],R:(ring?)): bool = subset?(S,R) AND ring?(S)

END ring_def