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