Quelle  fun_preds_partial.pvs   Sprache: unbekannt

%------------------------------------------------------------------------------
% partial order properties on functions
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            14/06/09  Initial Version
%------------------------------------------------------------------------------
fun_preds_partial[T1,T2:TYPE,le1:(partial_order?[T1]),
                             le2:(partial_order?[T2])]: THEORY

BEGIN

  f:   VAR [T1->T2]
  x,y: VAR T1
  a,b: VAR T2

  lt1(x,y)  : MACRO bool = le1(x,y) AND x /= y
  lt2(a,b)  : MACRO bool = le2(a,b) AND a /= b

  increasing?(f)        : bool = FORALL x, y : le1(x,y) IMPLIES le2(f(x),f(y))
  decreasing?(f)        : bool = FORALL x, y : le1(x,y) IMPLIES le2(f(y),f(x))
  strict_increasing?(f) : bool = FORALL x, y : lt1(x,y) IMPLIES lt2(f(x),f(y))
  strict_decreasing?(f) : bool = FORALL x, y : lt1(x,y) IMPLIES lt2(f(y),f(x))

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

  monotonic?(f)         : bool = increasing?(f) OR decreasing?(f)
  strict_monotonic?(f)  : bool = strict_increasing?(f) OR strict_decreasing?(f)

  strict_increasing_is_increasing:
        LEMMA strict_increasing?(f) IMPLIES increasing?(f)

  strict_decreasing_is_decreasing:
        LEMMA strict_decreasing?(f) IMPLIES decreasing?(f)

END fun_preds_partial