bound_defs[T: TYPE, S: TYPEFROM 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
¤ 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.0.13Bemerkung:
(vorverarbeitet)
¤
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.
