|
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
¤ 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.
|
