%------------------------------------------------------------------------------
% Definitions and subtype properties of directed complete partial orders
%
%       Author: David Lester <dlester@cs.man.ac.uk> Manchester University
%
%       Version 1.0          02/09/06 
%------------------------------------------------------------------------------

directed_orders[T:TYPE]: THEORY

BEGIN

  IMPORTING relations_extra[T]

  x,y,z: VAR T
  p:     VAR pred[[T,T]]
  <=:    VAR (partial_order?[T])
  S:     VAR (nonempty?[T])
  X:     VAR set[T]

  IMPORTING bounded_orders[T], chain, ordered_subset[T]

  trivial_partial_order?(p):bool = FORALL x,y: p(x,y) IFF x = y

  directed?(<=)(S):bool
    = FORALL x,y: S(x) AND S(y) IMPLIES EXISTS (z:(S)): x <= z AND y <= z

  directed?(<=,S):MACRO bool = directed?(<=)(S)

  directed_def: LEMMA FORALL (D:(directed?(<=))):
      FORALL X: is_finite(X) AND subset?(X,D) IMPLIES
         EXISTS (x:(D)): bounded_orders.upper_bound?(x,X,<=)

  directed_complete?(<=):bool
    = FORALL (D:(directed?(<=))): least_bounded_above?(<=)(D)

  directed_complete_partial_order?(p):bool
    = partial_order?(p) AND directed_complete?(p)

  chain_complete?(<=):bool
    = FORALL (C:(chain?[T,(<=)])): least_bounded_above?(<=)(C)

  chain_complete_partial_order?(p):bool
    = partial_order?(p) AND chain_complete?(p)

  directed_least_bounded_above: LEMMA
    FORALL (<=:(directed_complete_partial_order?), D:(directed?(<=))):
            least_bounded_above?(<=)(D)

  dcpo_is_po: JUDGEMENT (directed_complete_partial_order?) SUBTYPE_OF
                                                             (partial_order?)

  complete_upper_semilattice_is_dcpo:
              JUDGEMENT (complete_upper_semilattice?) SUBTYPE_OF
                        (directed_complete_partial_order?)

  IMPORTING minmax_orders[T]

  pointed_directed_complete_partial_order?(p): bool
    = directed_complete_partial_order?(p) AND has_least?(p)(fullset[T])

  pdcpo_is_dcpo: JUDGEMENT (pointed_directed_complete_partial_order?)
                                 SUBTYPE_OF (directed_complete_partial_order?)

  pdcpo_is_ccpo: JUDGEMENT (pointed_directed_complete_partial_order?)
                                 SUBTYPE_OF (chain_complete_partial_order?)

END directed_orders