funinverse {X, YB : TYPE; yb : YB} : CONTEXT =
BEGIN

%%  The special function inverse context, which models 
%%  the inverse operation for Z injective functions, which 
%%  are guaranteed to have an inverse that is a function 
%%  (rather than a relation, the general case).

%% Version revised by A J H Simons on 13 March 2014.

%%  Local types - do not export; for internal use within 
%%  this context only.

	Y : TYPE = {y : YB | y /= yb};

	Function : TYPE = [X -> YB];
	Inverse : TYPE = [Y -> X];

%%  The inverse function operation can only be expressed 
%%  in SAL as a relational constraint linking a function 
%%  and its inverse.  This encoding assumes that fun is
%%  injective (a precondition).  Together, fun and inv
%%  form a (possibly partial) bijection.

   inverse (fun : Function, inv : Inverse) : BOOLEAN =
      FORALL (x : X) :  FORALL (y : Y) :
         (fun(x) = y) = (inv(y) = x);
END