% Lattices that have a "complement" function. See also complementary_orders.
%

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

BEGIN

  IMPORTING
    lattices[T, <=],
    minmax_orders[T],
    function_image_extra[T, T],
    complementary_orders[T]

  t, t1, t2: VAR T
  C, H: VAR [T -> T]
  S: VAR set[T]
  NF: VAR non_empty_finite_set[T]

%   modular?(<=): bool =
%     FORALL (a, c: T):
%       a <= c => lub(<=)(a, glb(<=)(b, c)) = glb(<=)(lub(<=)(a, b), c)

  dual(C)(H): [T -> T] = C o H o C

  dual_dual : LEMMA
    FORALL (C: (complement?(<=))): dual(C)(dual(C)(H)) = H

  dual_inclusion1 : LEMMA
    FORALL (C: (complement?(<=))): H(C(t)) <= C(t) IFF t <= dual(C)(H)(t)

  dual_inclusion2 : LEMMA
    FORALL (C: (complement?(<=))): C(t) <= H(C(t)) IFF dual(C)(H)(t) <= t

  dual_inclusion3 : LEMMA
    FORALL (C: (complement?(<=))): H(t) <= t IFF C(t) <= dual(C)(H)(C(t))

  dual_inclusion4 : LEMMA
    FORALL (C: (complement?(<=))): t <= H(t) IFF dual(C)(H)(C(t)) <= C(t)


END complementary_lattices