|
bound_defs[T: TYPE, S: TYPE FROM T]: THEORY
%------------------------------------------------------------------------
%
% The following definitions are very similar to the definitions in the
% prelude theory orders. There is an important distinctions. pe is defined
% as
%
% pe: VAR pred[S]
%
% rather than
%
% pe: VAR {p: pred[T] | EXISTS (x: T): p(x)}
%
% this prevents the proliferation of superfluous "extend"s
%
%------------------------------------------------------------------------
BEGIN
< : VAR pred[[T, T]]
pe: VAR pred[S]
x,y: VAR T
z: VAR S
upper_bound(<)(x, pe): bool = FORALL (z: (pe)): z < x
lower_bound(<)(x, pe): bool = FORALL (z: (pe)): x < z
least_upper_bound(<)(x, pe): bool =
upper_bound(<)(x, pe) AND
(FORALL y: upper_bound(<)(y, pe) IMPLIES (x < y OR x = y))
greatest_lower_bound(<)(x, pe): bool =
lower_bound(<)(x, pe) AND
(FORALL y: lower_bound(<)(y, pe) IMPLIES (y < x OR x = y))
END bound_defs
¤ Dauer der Verarbeitung: 0.16 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.
|
