SSL operator_defs_more.pvs

%------------------------------------------------------------------------------
% Extras for operator_def file
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            5/5/04   DRL
%------------------------------------------------------------------------------

operator_defs_more[T: TYPE]: THEORY

  BEGIN
  o,*:   VAR [T,T->T]
  x,y,z: VAR T

  closed_operator?(o)     : bool = (FORALL x,y:   member(x o y, fullset[T]))
  right_distributive?(*,o): bool = (FORALL x,y,z: x*(y o z) = (x*y) o (x*z))
  left_distributive?(*,o) : bool = (FORALL x,y,z: (x o y)*z = (x*z) o (y*z))

  commutative_over?(S:set[T])(*) : bool
     = (FORALL x,y:   member(x,S) AND member(y,S) IMPLIES x*y = y*x)
  associative_over?(S:set[T])(*) : bool
     = (FORALL x,y,z: member(x,S) AND member(y,S) AND member(z,S) IMPLIES
                                                         (x*y)*z = x*(y*z))

  END operator_defs_more