|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
