%------------------------------------------------------------------------------
%
% These are properties of bounded partial orders. Because we're importing the
% the partial order, it needn't clutter up the theories.
%
% We're defining the least_upper_bound and greatest_lower_bound operators
% (lub(S) and glb(S) respectively) for all suitable sets S. Notice that they
% needn't be nonempty.
%
%------------------------------------------------------------------------------

bounded_order_props[T:TYPE,<=:(partial_order?[T])]: THEORY

BEGIN

  IMPORTING sets[T], bounded_orders[T]

  x,y:   VAR T
  S,A,B: VAR set[T]

  above?(A,B): bool = FORALL (x:(B)): EXISTS (y:(A)): x <= y
  below?(A,B): bool = FORALL (x:(B)): EXISTS (y:(A)): y <= x

  lub_set?(S):bool = least_bounded_above?(<=)(S)

  singleton_is_lub_set: JUDGEMENT (singleton?) SUBTYPE_OF (lub_set?)

  SA,XA,YA: VAR (lub_set?)

  lub(SA): {x | bounded_orders[T].least_upper_bound?(x,SA,<=)}

  lub_rew: LEMMA lub(SA) = lub(<=)(SA)

  lub_singleton: LEMMA lub(singleton(x)) = x

  lub_lem: LEMMA lub(SA) = x IFF bounded_orders[T].least_upper_bound?(x,SA,<=)

  above_lub: LEMMA above?(XA,YA) IMPLIES lub(YA) <= lub(XA)

  glb_set?(S):bool = bounded_orders[T].greatest_bounded_below?(<=)(S)

  singleton_is_glb_set: JUDGEMENT (singleton?) SUBTYPE_OF (glb_set?)

  SB,XB,YB: VAR (glb_set?)

  glb(SB): {x | bounded_orders[T].greatest_lower_bound?(x,SB,<=)}

  glb_rew: LEMMA glb(SB) = glb(<=)(SB)

  glb_singleton: LEMMA glb(singleton(x)) = x

  glb_lem: LEMMA glb(SB) = x IFF
                           bounded_orders[T].greatest_lower_bound?(x,SB,<=)

  below_glb: LEMMA below?(XB,YB) IMPLIES glb(XB) <= glb(YB)

END bounded_order_props