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

%% The function context, which models Z partial functions as total SAL
%% functions.  The domain type is X (with no bottom); the range type is
%% YB, which extends the type Y with a bottom element yb.

%% This improved version of the function only requires one bottom value for
%% the range type.  This simplifies the definition of many operations, which
%% no longer need a special case for undefined domain values.

%% Version revised by A J H Simons on 1 September 2011.

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

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

	XY : TYPE = [X, Y];
	YX : TYPE = [Y, X];
	
	Relation : TYPE = [XY -> BOOLEAN];  	%% set{XY;}!Set
	Inverse : TYPE = [YX -> BOOLEAN];   	%% set{YX;}!Set
	
	Domain : TYPE = [X -> BOOLEAN];     	%% set{X;}!Set
	Range : TYPE = [Y -> BOOLEAN];      	%% set{Y;}!Set

%% Exported type - use only if you don't want to apply operations from other
%% contexts as well.  If you do, use the base type [X -> YB].

	Function : TYPE = [X -> YB];

%% Function constructors.  An empty function is a map from every domain value
%% to the bottom range value.  A singleton is a function containing a single
%% pair.  A maplet is another way to construct a singleton with given domain
%% and range values.  Note that some function types may not be empty - total,
%% surjective and bijective functions must be defined for the whole range.

	empty : Function =
		LAMBDA (x : X) : yb;
		
	singleton (pair : XY) : Function = 
		LAMBDA (x : X) : IF x = pair.1 
			THEN pair.2 ELSE yb ENDIF;

	maplet (x : X, y : Y) : Function =
		LAMBDA (f : X) : IF f = x 
			THEN y ELSE yb ENDIF;
		
%% Set-like predicates on a function.  Replicated for efficiency to save
%% converting a function back to a set.

	empty? (fun : Function) : BOOLEAN = 
		FORALL (x : X) : fun(x) = yb;
		
 	contains? (fun : Function, pair : XY) : BOOLEAN =
		fun(pair.1) = pair.2;

	subset? (funA, funB : Function) : BOOLEAN =
		FORALL (x : X) : LET y : YB = funA(x) IN
			y = yb OR y = funB(x);

	properSubset? (funA, funB : Function) : BOOLEAN =
		subset? (funA, funB) AND EXISTS (x : X) :
			funA(x) = yb AND funB(x) /= yb;

%% Function-type predicates on a function.  These are provided for use where
%% Z declares different function types, and may be added to the invariant.
%% By default, functions are naturally partial, but may grow to become total:
%% the Z definition of partial functions *includes* the total functions.  The
%% injective? predicate asserts that every valid x maps to a unique y, while
%% surjective? asserts that all y are covered by a mapping from some x, and
%% bijective? asserts both these properties.  For convenience, combinations
%% of total? with other properties are also given.

	partial? (fun : Function) : BOOLEAN = TRUE;

	total? (fun : Function) : BOOLEAN =
		FORALL (x : X) : fun(x) /= yb;

	injective? (fun : Function) : BOOLEAN =
		FORALL (x1, x2 : X) : LET y : YB = fun(x1) IN
			y = yb OR y /= fun(x2) OR x1 = x2;
	
	surjective? (fun : Function) : BOOLEAN =
		FORALL (y : Y) : EXISTS (x : X) : fun(x) = y;

	bijective? (fun : Function) : BOOLEAN =
		injective? (fun) AND surjective? (fun);

	totalInjective? (fun : Function) : BOOLEAN =
		FORALL (x1, x2 : X) : LET y : YB = fun(x1) IN
			y /= yb AND (y /= fun(x2) OR x1 = x2);

	totalSurjective? (fun : Function) : BOOLEAN =
		total? (fun) AND surjective? (fun);

	totalBijective? (fun : Function) : BOOLEAN = 
		total? (fun) AND bijective? (fun);
		
%% Relational operations for domain, range, image and inverse relation.
%% Replicated for efficiency to save converting a function back to a set.
%% If the function is injective, the inverse relation may be converted back
%% to a function, if so desired, using the convert(fun) = rel equivalence.
	
	domain (fun : Function) : Domain = 
		LAMBDA (x : X) : fun(x) /= yb;

	range (fun : Function) : Range = 
		LAMBDA (y : Y) : EXISTS (x : X) : fun(x) = y;
		
	image (fun : Function, set : Domain) : Range =
		LAMBDA (y : Y) : EXISTS (x : X) : 
			set(x) AND fun(x) = y;
		
	inverse (fun : Function) : Inverse =
		LAMBDA (pair : YX) : fun(pair.2) = pair.1;

%% Relational operations for restriction and subtraction (anti-restriction).
%% Replicated for efficiency to save converting a function back to a set.

%% Note in rangeRestrict and rangeSubtract that set : [Y -> BOOLEAN] seems
%% happy to accept values y : YB from the extended type (viz. Y <= YB). SAL
%% may coerce subtypes to their base type, with a membership restriction.

	domainRestrict (set : Domain, fun : Function) : Function =
		LAMBDA (x : X) : IF set(x)
			THEN fun(x) ELSE yb ENDIF;
	
	domainSubtract (set : Domain, fun : Function) : Function =
		LAMBDA (x : X) : IF set(x)
			THEN yb ELSE fun(x) ENDIF;

	rangeRestrict (fun : Function, set : Range) : Function =
		LAMBDA (x : X) : LET y : YB = fun(x) IN
			IF set(y) THEN y ELSE yb ENDIF;	   %% no type error!

	rangeSubtract (fun : Function, set : Range) : Function =
		LAMBDA (x : X) : LET y : YB = fun(x) IN
			IF set(y) THEN yb ELSE y ENDIF;	    %% no type error!

%% Function union, override and difference.  The simple union and difference
%% operations are replicated for efficiency to save converting a function
%% back to a set.  Override replaces maplets in funA by maplets in funB that
%% share the same domain value.  Special optimised versions insert(fun, pair)
%% and remove(fun, pair) are given, for use when Z has override or difference
%% with a singleton pair, representing a maplet.  A more convenient version 
%% insertMaplet(fun, dom, ran) saves constructing the singleton.  The special 
%% optimised version removeDomain(fun, dom) performs domain subtraction with
%% a single domain value, to save constructing a singleton set.

	union (funA, funB : Function) : Relation =
		LAMBDA (pair : XY) : funA(pair.1) = pair.2
			OR funB(pair.1) = pair.2;

	difference (funA, funB : Function) : Function =
		LAMBDA (x : X) : LET y : YB = funA(x) IN
			IF y = funB(x) THEN yb ELSE y ENDIF;

	override (funA, funB : Function) : Function =
		LAMBDA(x : X) : LET y : YB = funB(x) IN
			IF y = yb THEN funA(x) ELSE y ENDIF;

	insert (fun : Function, pair : XY) : Function =
		LAMBDA (x : X) : IF x = pair.1
			THEN pair.2 ELSE fun(x)	ENDIF;

	remove (fun : Function, pair : XY) : Function = 
		LAMBDA (x : X) : LET y : YB = fun(x) IN
			IF x = pair.1 AND y = pair.2
				THEN yb ELSE y ENDIF;
	
	insertMaplet (fun : Function, dom : X, ran : Y) : Function =
		LAMBDA (x : X) : IF x = dom 
			THEN ran else fun(x) ENDIF;
		
	removeDomain (fun : Function, val : X) : Function =
		LAMBDA (x : X) : IF x = val
			THEN yb	ELSE fun(x) ENDIF;	

%% Convert a function back to a relation, for the sake of using any
%% set-theoretic operations not defined explicitly for functions. This
%% conversion is expensive, so should be avoided if possible.
		
	convert (fun : Function) : Relation =
		LAMBDA (pair : XY) : fun(pair.1) = pair.2;

END