FDL > PVS > Prelude > operator_defs : Theory

PVS-2.4 prelude.pvs

operator_defs [T:TYPE] : THEORY
BEGIN

O: VAR [T, T- > T]

*: VAR [T, T- > T]

-: VAR [T- > T]

x: VAR T

y: VAR T

z: VAR T

commutative?(O): bool = FORALL x, y : (x O y) = (y O x);

associative?(O): bool = FORALL x, y, z : (x O y O z) = (x O (y O z));

left identity?(O)(y): bool = FORALL x : (y O x) = x;

right identity?(O)(y): bool = FORALL x : (x O y) = x;

identity?(O)(y): bool = FORALL x : ((x O y) = x) AND ((y O x) = x);

has identity?(O): bool = EXISTS y : identity?(O)(y);

zero?(O)(y): bool = FORALL x : ((x O y) = y) AND ((y O x) = y);

has zero?(O): bool = EXISTS y : zero?(O)(y);

inverses?(O)(-)(y): bool = FORALL x : ((x O (-x)) = y) AND (((-x) O x) = y);

has inverses?(O): bool = EXISTS -, y : inverses?(O)(-)(y);

distributive?(*, O): bool = FORALL x, y, z : (x * (y O z)) = ((x * y) O (x * z));

END operator_defs