% orders on a finite type have special properties:
% e.g., every lattice is complete; every strict-order is well-founded.
%
% Author: Alfons Geser, National Institute of Aerospace
% Date: Dec 2004/Jan 2005

finite_orders[T: TYPE+]: THEORY

BEGIN

ASSUMING

  finite_type: ASSUMPTION is_finite_type[T]

ENDASSUMING

  IMPORTING bounded_orders[T], finite_types[T]

  R: VAR pred[[T, T]]
  S: VAR (nonempty?[T])  % used in proofs

  % lattice properties

  finite_lower_semilattice_is_complete: LEMMA
    greatest_bounded_below?(R)(emptyset) & lower_semilattice?(R) =>
      complete_lower_semilattice?(R)

  finite_upper_semilattice_is_complete: LEMMA
    least_bounded_above?(R)(emptyset) & upper_semilattice?(R) =>
      complete_upper_semilattice?(R)

  finite_lattice_is_complete: JUDGEMENT
    (lattice?) SUBTYPE_OF (complete_lattice?)

  % well-foundedness properties

  finite_strict_order_is_well_founded: JUDGEMENT
    (strict_order?) SUBTYPE_OF (well_founded?[T])

  finite_strict_total_order_is_well_ordered: JUDGEMENT
    (strict_total_order?) SUBTYPE_OF (well_ordered?[T])

END finite_orders