Quelle  real_fun_preds.pvs

real_fun_preds [T : TYPE FROM real] : THEORY
%----------------------------------------------------------------------%
%  Defines several predicates over real-valued functions [T -> real]   %
%
%  These predicates now follow ? convention.
%  Old names without ? are included as macros to maintain upwards-
%  compatibility.
%
%----------------------------------------------------------------------%
BEGIN

  f    : VAR [T -> real]
  x, y : VAR T
  a, z : VAR real
  E    : VAR setof[real]

  increasing?(f)        : bool = FORALL x, y : x <= y IMPLIES f(x) <= f(y)
  decreasing?(f)        : bool = FORALL x, y : x <= y IMPLIES f(y) <= f(x)
  strict_increasing?(f) : bool = FORALL x, y : x < y IMPLIES f(x) < f(y)
  strict_decreasing?(f) : bool = FORALL x, y : x < y IMPLIES f(y) < f(x)

  monotonic?(f): bool = increasing?(f) or decreasing?(f)

  constant?(f)          : bool = FORALL x, y : f(x) = f(y)

  is_maximum?(x, f)     : bool = FORALL y : f(y) <= f(x)
  is_minimum?(x, f)     : bool = FORALL y : f(x) <= f(y)

  bounded_above?(f)     : bool = EXISTS a: FORALL x: f(x) <= a
  bounded_below?(f)     : bool = EXISTS a: FORALL x: a <= f(x)
  bounded?(f)           : bool = bounded_above?(f) AND bounded_below?(f)

  bounded?_lem          : LEMMA bounded?(f) IFF
                               EXISTS (B: nnreal): FORALL x: abs(f(x)) <= B



% ------- The following are included to maintain upwards compatibility 
% ------- with previous versions of libraries 

  increasing(f)         : MACRO bool = increasing?(f)
  decreasing(f)         : MACRO bool = decreasing?(f)
  strict_increasing(f)  : MACRO bool = strict_increasing?(f)
  strict_decreasing(f)  : MACRO bool = strict_decreasing?(f) 
  constant(f)           : MACRO bool = constant?(f)   
  is_maximum(x,f)       : MACRO bool = is_maximum?(x,f)
  is_minimum(x,f)       : MACRO bool = is_minimum?(x,f)


END real_fun_preds