Quelle  complementary_orders.pvs   Sprache: PVS

% Ordered sets (T, <=) that have a "complement" function, i.e.,
% an involutorian, anti-monotone function from T to T.
%

complementary_orders[T: TYPE+]: THEORY

BEGIN

  IMPORTING bounded_orders[T]

  rel: VAR pred[[T, T]]
  C: VAR [T -> T]
  t, t1, t2: VAR T
  S: VAR set[T]

  complement?(rel)(C): bool =
    C o C = id[T] & preserves(C, rel, converse(rel))

%   complement_is_bijective: JUDGEMENT
%     (complement?(rel)) SUBTYPE_OF (bijective?[T, T])

  complement_complement: LEMMA
    FORALL (C: (complement?(rel))): C(C(t)) = t

  image_complement: LEMMA
    FORALL (C: (complement?(rel))): image(C, image(C, S)) = S

  inverse_complement: LEMMA
    FORALL (C: (complement?(rel))): inverse[T, T](C) = C

%   inverse_complement_is_complement: JUDGEMENT
%     inverse[T, T](C: (complement?(rel))) HAS_TYPE (complement?(rel))

  le_complement: LEMMA
    FORALL (C: (complement?(rel))): rel(C(t1), C(t2)) IFF rel(t2, t1)

  upper_bound_complement: LEMMA
    FORALL (C: (complement?(rel))):
      upper_bound?[T](t, S, rel) IFF lower_bound?[T](C(t), image(C, S), rel)

  bounded_above_complement: LEMMA
    FORALL (C: (complement?(rel))):
      bounded_above?[T](S, rel) IFF bounded_below?[T](image(C, S), rel)

  least_upper_bound_complement: LEMMA
    FORALL (C: (complement?(rel))):
      least_upper_bound?[T](t, S, rel) IFF
      greatest_lower_bound?[T](C(t), image(C, S), rel)

  least_bounded_above_complement: LEMMA
    FORALL (C: (complement?(rel))):
      least_bounded_above?[T](S, rel) IFF
      greatest_bounded_below?[T](image(C, S), rel)

  lub_complement: LEMMA
    FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)),
            S: (least_bounded_above?(rel))):
      lub[T](rel)(S) = C(glb[T](rel)(image(C, S)))

  glb_complement: LEMMA
    FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)),
            S: (greatest_bounded_below?(rel))):
      glb[T](rel)(S) = C(lub[T](rel)(image(C, S)))

END complementary_orders