Quelle relations_extra.pvs Sprache: 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

quality37%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.