Quelle  const_fun_def.pvs

%------------------------------------------------------------------------------
% Generalised constant functions
%
% Generalises real constant functions.
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            8/10/04  Initial Version
%     Version 1.0            8/10/04  Generalised (inverse-)image
%------------------------------------------------------------------------------

const_fun_def[S,T:TYPE]: THEORY

BEGIN

  x: VAR S
  a: VAR T
  X: VAR set[S]
  Y: VAR set[T]

  const_fun(a): [S->T] = LAMBDA x : a

  constant?(f:[S->T]):bool = EXISTS a: f = const_fun(a)

  image_const: LEMMA
     image(const_fun(a),X)
        = IF empty?(X) THEN emptyset[T] ELSE singleton(a) ENDIF

  inverse_image_const: LEMMA
     inverse_image(const_fun(a),Y)
        = IF Y(a) THEN fullset[S] ELSE emptyset[S] ENDIF

END const_fun_def