%-------------------------------------------------------------------------
%
% "Stronger" and "weaker" orders. Given two relations on T, rel1 and
% rel2, if strict_subset?(rel1, rel2), then we say that rel1 is
% weaker than rel2, and that rel2 is stronger than rel1. If
% subset?(rel1, rel2), then rel1 is weaker than or equal to rel2, and
% rel2 is stronger than or equal to rel1.
%
% For PVS version 3.2. January 14, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% orders: order_strength[T]
%
%-------------------------------------------------------------------------
order_strength[T: TYPE]: THEORY
BEGIN
t1, t2: VAR T
ord1, ord2: VAR pred[[T, T]]
% Stronger orders: if ord1 is stronger than ord2, then ord1 orders every
% pair of elements that ord2 orders
stronger_eq?(ord1, ord2): MACRO bool = subset?(ord2, ord1)
stronger_eq?(ord2)(ord1): MACRO bool = subset?(ord2, ord1)
stronger?(ord1, ord2): MACRO bool = strict_subset?(ord2, ord1)
stronger?(ord2)(ord1): MACRO bool = strict_subset?(ord2, ord1)
% Weaker orders: if ord1 is weaker than ord2, then ord2 orders every
% pair of elements that ord1 orders
weaker_eq?(ord1, ord2): MACRO bool = subset?(ord1, ord2)
weaker_eq?(ord2)(ord1): MACRO bool = subset?(ord1, ord2)
weaker?(ord1, ord2): MACRO bool = strict_subset?(ord1, ord2)
weaker?(ord2)(ord1): MACRO bool = strict_subset?(ord1, ord2)
% ==========================================================================
% Properties preserved by stronger/weaker orders
% ==========================================================================
stronger_reflexive: THEOREM
FORALL ord1, ord2:
stronger_eq?(ord1, ord2) AND reflexive?(ord2) => reflexive?(ord1)
weaker_irreflexive: THEOREM
FORALL ord1, ord2:
weaker_eq?(ord1, ord2) AND irreflexive?(ord2) => irreflexive?(ord1)
weaker_antisymmetric: THEOREM
FORALL ord1, ord2:
weaker_eq?(ord1, ord2) AND antisymmetric?(ord2) =>
antisymmetric?(ord1)
END order_strength
¤ Dauer der Verarbeitung: 0.20 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.
|
