Quelle  monotone_functions.pvs

%-------------------------------------------------------------------------
%
%  Monotonically increasing, decreasing, nonincreasing, and nondecreasing
%  functions.
%
%  For PVS version 3.2.  January 13, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[D], orders[R], relation_props2[D, D, D, D],
%    relation_props2[R, R, R, R], relations[D], relations[R]
%  orders: closure_ops[D], closure_ops[R], indexed_sets_extra,
%    monotone_functions[D,R], relation_iterate[D], relation_iterate[R],
%    relations_extra[D], relations_extra[R]
%
%-------------------------------------------------------------------------
monotone_functions[D: TYPE, R: TYPE]: THEORY
 BEGIN

  IMPORTING closure_ops[D], closure_ops[R]

  d1, d2: VAR D
  r1, r2: VAR R
  f: VAR [D -> R]
  Drel: VAR pred[[D, D]]
  Rrel: VAR pred[[R, R]]
  Dtot: VAR (total_order?[D])
  Dstr: VAR (strict_total_order?[D])

  increasing?(Drel, Rrel)(f): bool =
      preserves(f, irreflexive_kernel(Drel), irreflexive_kernel(Rrel))

  nonincreasing?(Drel, Rrel)(f): bool =
      inverts(f, reflexive_closure(Drel), reflexive_closure(Rrel))

  decreasing?(Drel, Rrel)(f): bool =
      inverts(f, irreflexive_kernel(Drel), irreflexive_kernel(Rrel))

  nondecreasing?(Drel, Rrel)(f): bool =
      preserves(f, reflexive_closure(Drel), reflexive_closure(Rrel))

  increasing_is_nondecreasing: THEOREM
    FORALL Drel, Rrel, f:
      increasing?(Drel, Rrel)(f) IMPLIES nondecreasing?(Drel, Rrel)(f)

  decreasing_is_nonincreasing: THEOREM
    FORALL Drel, Rrel, f:
      decreasing?(Drel, Rrel)(f) IMPLIES nonincreasing?(Drel, Rrel)(f)

  not_increasing_and_nonincreasing: THEOREM
    (EXISTS d1, d2: d1 /= d2) IMPLIES
     (FORALL (Drel: (trichotomous?[D])), (Rrel: (antisymmetric?[R])), f:
        NOT (increasing?(Drel, Rrel)(f) AND nonincreasing?(Drel, Rrel)(f)))

  not_decreasing_and_nondecreasing: THEOREM
    (EXISTS d1, d2: d1 /= d2) IMPLIES
     (FORALL (Drel: (trichotomous?[D])), (Rrel: (antisymmetric?[R])), f:
        NOT (decreasing?(Drel, Rrel)(f) AND nondecreasing?(Drel, Rrel)(f)))

  increasing_converse_decreasing1: THEOREM
    FORALL Drel, Rrel:
      increasing?(Drel, Rrel) = decreasing?(Drel, converse(Rrel))

  increasing_converse_decreasing2: THEOREM
    FORALL Drel, Rrel:
      increasing?(Drel, Rrel) = decreasing?(converse(Drel), Rrel)

  nonincreasing_converse_nondecreasing1: THEOREM
    FORALL Drel, Rrel:
      nonincreasing?(Drel, Rrel) = nondecreasing?(Drel, converse(Rrel))

  nonincreasing_converse_nondecreasing2: THEOREM
    FORALL Drel, Rrel:
      nonincreasing?(Drel, Rrel) = nondecreasing?(converse(Drel), Rrel)

  increasing_total_order_injective: THEOREM
    FORALL Dtot, Rrel, f: increasing?(Dtot, Rrel)(f) IMPLIES injective?(f)

  increasing_strict_total_order_injective: THEOREM
    FORALL Dstr, Rrel, f: increasing?(Dstr, Rrel)(f) IMPLIES injective?(f)

  decreasing_total_order_injective: THEOREM
    FORALL Dtot, Rrel, f: decreasing?(Dtot, Rrel)(f) IMPLIES injective?(f)

  decreasing_strict_total_order_injective: THEOREM
    FORALL Dstr, Rrel, f: decreasing?(Dstr, Rrel)(f) IMPLIES injective?(f)

 END monotone_functions