|
fun_preds_partial[T1,T2:TYPE,le1:(partial_order?[T1]),
le2:(partial_order?[T2])]: THEORY
BEGIN
f,g,h: 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
min(x,y):T1 = IF le1(x,y) THEN x ELSE y ENDIF
max(x,y):T1 = IF le1(x,y) THEN x ELSE y ENDIF
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)
min(f,g):[T1->T2] = LAMBDA x: IF le2(f(x),g(x)) THEN f(x) ELSE g(x) ENDIF
max(f,g):[T1->T2] = LAMBDA x: IF le2(f(x),g(x)) THEN g(x) ELSE f(x) ENDIF
mid(g,f,h):[T1->T2] = min(max(g,f),h)
increasing_is_function: JUDGEMENT (increasing?) SUBTYPE_OF [T1->T2]
decreasing_is_function: JUDGEMENT (decreasing?) SUBTYPE_OF [T1->T2]
constant_is_function : JUDGEMENT (constant?) SUBTYPE_OF [T1->T2]
monotonic_is_function : JUDGEMENT (monotonic?) SUBTYPE_OF [T1->T2]
strict_increasing_is_increasing:
JUDGEMENT (strict_increasing?) SUBTYPE_OF (increasing?)
strict_decreasing_is_decreasing:
JUDGEMENT (strict_decreasing?) SUBTYPE_OF (decreasing?)
strict_monotonic_is_monotonic:
JUDGEMENT (strict_monotonic?) SUBTYPE_OF (monotonic?)
% min_preserves_increasing: JUDGEMENT
END fun_preds_partial
¤ Dauer der Verarbeitung: 0.5 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.
|
