Quelle  lattices.pvs

% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004
%
% add_preserves_tightly_bounded and union_preserves_tightly_bounded added
% 13 Jan 2005 by Jerry James (jamesj@acm.org)

lattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (lattice?[T])
]: THEORY

BEGIN

  IMPORTING
    lower_semilattices[T, <=],
    upper_semilattices[T, <=]

  t: VAR T
  tb, tb2: VAR (tightly_bounded?(<=))

  finite_set_is_tightly_bounded: JUDGEMENT
    non_empty_finite_set[T] SUBTYPE_OF (tightly_bounded?(<=))

  add_preserves_tightly_bounded: JUDGEMENT
    add(t, tb) HAS_TYPE (tightly_bounded?(<=))

  union_preserves_tightly_bounded: JUDGEMENT
    union(tb, tb2) HAS_TYPE (tightly_bounded?(<=))

END lattices