Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: relations_extra.pvs Sprache: PVS

Original von: PVS^©

%
%
% Purpose: rewrite rules for the properties that
%          binary relations may have
%
% Author: Alfons Geser ([email protected]), NIA
%
%

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]

  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?)

  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

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

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

  reflexive_closure(R): (reflexive?) = union(R, =)
  irreflexive_kernel(R): (irreflexive?) = difference(R, =)
  symmetric_closure(R): (symmetric?) = union(R, converse(R))
  symmetric_kernel(R): (symmetric?) = intersection(R, converse(R))

  reflexive_closure_preserves_transitive: JUDGEMENT
    reflexive_closure(R: (transitive?)) HAS_TYPE (preorder?)

  strict_order_to_partial_order: JUDGEMENT
    reflexive_closure(R: (strict_order?)) HAS_TYPE (partial_order?)

  reflexive_closure_dichotomous: JUDGEMENT
    reflexive_closure(R: (trichotomous?)) HAS_TYPE (dichotomous?)

  strict_total_order_to_total_order: JUDGEMENT
    reflexive_closure(R: (strict_total_order?)) HAS_TYPE (total_order?)

  partial_order_to_strict_order: JUDGEMENT
    irreflexive_kernel(R: (partial_order?)) HAS_TYPE (strict_order?)

  irreflexive_kernel_trichotomous: JUDGEMENT
    irreflexive_kernel(R: (dichotomous?)) HAS_TYPE (trichotomous?)

  total_order_to_strict_total_order: JUDGEMENT
    irreflexive_kernel(R: (total_order?)) HAS_TYPE (strict_total_order?)

  symmetric_kernel_of_preorder: JUDGEMENT
    symmetric_kernel(R: (preorder?)) HAS_TYPE (equivalence?)

END relations_extra

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.