%
%
% 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.6 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.
|
