Quelle  relations_extra.pvs

%-------------------------------------------------------------------------
%
%  Definitions of asymmetric? and order?, along with judgements for the
%  properties that binary relations may have.  Alfons Geser wrote the
%  definition of asymmetric?, the judgements dealing with asymmetric?,
%  and dichotomous_is_trichotomous in Oct. 2004.  Jerry James wrote the
%  rest at various times.
%
%  For PVS version 3.2.  February 23, 2005
%  ---------------------------------------------------------------------
%      Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[T], relations[T]
%  orders: relations_extra[T]
%
%-------------------------------------------------------------------------
relations_extra[T: TYPE]: THEORY

BEGIN

  IMPORTING relations[T], orders[T]

  x, y, z: VAR T
  R: VAR pred[[T, T]]
  p: VAR pred[T]


  % ==========================================================================
  % Asymmetry
  % ==========================================================================

  asymmetric?(R): bool = FORALL x, y: NOT R(x, y) OR NOT R(y, x)

  strict_order_is_asymmetric: JUDGEMENT
    (strict_order?) SUBTYPE_OF (asymmetric?)

  asymmetric_is_antisymmetric: JUDGEMENT
    (asymmetric?) SUBTYPE_OF (antisymmetric?)

  asymmetric_is_irreflexive: JUDGEMENT
    (asymmetric?) SUBTYPE_OF (irreflexive?)


  % ==========================================================================
  % Dichotomous-trichotomous relationship
  % ==========================================================================

  dichotomous_is_trichotomous: JUDGEMENT
    (dichotomous?) SUBTYPE_OF (trichotomous?)


  % ==========================================================================
  % Orders: a generalization of partial and strict orders
  % ==========================================================================

  order?(R): bool = transitive?(R) AND antisymmetric?(R)

  order_is_transitive: JUDGEMENT (order?) SUBTYPE_OF (transitive?)

  order_is_antisymmetric: JUDGEMENT (order?) SUBTYPE_OF (antisymmetric?)

  partial_order_is_order: JUDGEMENT (partial_order?) SUBTYPE_OF (order?)

  strict_order_is_order: JUDGEMENT (strict_order?) SUBTYPE_OF (order?)


  % ==========================================================================
  % Linear orders: a generalization of total and strict_total orders
  % ==========================================================================

  linear_order?(R): bool = order?(R) AND trichotomous?(R)

  total_order_is_linear: JUDGEMENT (total_order?) SUBTYPE_OF (linear_order?)

  strict_total_order_is_linear: JUDGEMENT
    (strict_total_order?) SUBTYPE_OF (linear_order?)


  % ==========================================================================
  % Convenience lemmas
  % ==========================================================================

  reflexive: LEMMA FORALL (R: (reflexive?)): FORALL x: R(x, x)

  irreflexive: LEMMA FORALL (R: (irreflexive?)): FORALL x: NOT R(x, x)

  symmetric: LEMMA FORALL (R: (symmetric?)): FORALL x, y: R(x, y) => R(y, x)

  antisymmetric: LEMMA
    FORALL (R: (antisymmetric?)): FORALL x, y: R(x, y) & R(y, x) => x = y

  asymmetric: LEMMA
    FORALL (R: (asymmetric?)): FORALL x, y: NOT R(x, y) OR NOT R(y, x)

% connected? is the same as trichotomous?
%  connected: LEMMA FORALL (R: (connected?)): x = y OR R(x, y) OR R(y, x)

  transitive: LEMMA
    FORALL (R: (transitive?)): FORALL x, y, z: R(x, y) & R(y, z) => R(x, z)

  dichotomous: LEMMA
    FORALL (R: (dichotomous?)): FORALL x, y: R(x, y) OR R(y, x)

  trichotomous: LEMMA
    FORALL (R: (trichotomous?)): FORALL x, y: R(x, y) OR R(y, x) OR x = y

  well_founded: LEMMA
    FORALL (R: (well_founded?)):
      FORALL p:
        (EXISTS y: p(y)) IMPLIES
         (EXISTS (y: (p)): FORALL (x: (p)): NOT R(x, y))

END relations_extra