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