FDL > PVS > Prelude > relation_defs : Theory

PVS-2.4 prelude.pvs

 relation_defs defines operators on relations between possibly different
 types.  Note that some of the names are overloaded with those given in
 functions - in practice this should not cause any problems.

relation_defs [T1:TYPE, T2:TYPE] : THEORY
BEGIN

R: VAR pred[[T1, T2]]

X: VAR set[T1]

Y: VAR set[T2]

domain(R) : TYPE = {(x:T1) | EXISTS (y:T2) : R(x, y)}

range(R) : TYPE = {(y:T2) | EXISTS (x:T1) : R(x, y)}

image(R, X): set[T2] = {(y:T2) | EXISTS (x:(X) ) : R(x, y)};

image(R)(X): set[T2] = image(R, X);

preimage(R, Y): set[T1] = {(x:T1) | EXISTS (y:(Y) ) : R(x, y)};

preimage(R)(Y): set[T1] = preimage(R, Y);

postcondition(R, X): set[T2] = {(y:T2) | FORALL (x:(X) ) : R(x, y)};

postcondition(R)(X): set[T2] = postcondition(R, X);

precondition(R, Y): set[T1] = {(x:T1) | FORALL (y:(Y) ) : R(x, y)};

precondition(R)(Y): set[T1] = precondition(R, Y);

converse(R): pred[[T2, T1]] = LAMBDA (y:T2), (x:T1) : R(x, y);

isomorphism?(R): bool = EXISTS (f:(bijective?[T1, T2]) ) : R = graph(f);

total?(R): bool = FORALL (x:T1) : EXISTS (y:T2) : R(x, y);

onto?(R): bool = FORALL (y:T2) : EXISTS (x:T1) : R(x, y);

END relation_defs