%-------------------------------------------------------------------------
%
% 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 ([email protected]), National Institute of Aerospace
% Author: Jerry James ([email protected]), 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
