%-------------------------------------------------------------------------
%
% Isomorphisms between ordered sets. This is different than the
% isomorphism? predicate of relation_defs; that version says that a
% relation between two types is an isomorphism if it is a bijective
% function. This version says that a bijective function is an
% isomorphism with respect to relations on its domain and range types
% if it preserves those relations.
%
% For PVS version 3.2. February 24, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[D], orders[R], relations[D], relations[R]
% orders: isomorphism[D,R], relations_extra[D], relations_extra[R]
%
%-------------------------------------------------------------------------
isomorphism[D: TYPE, R: TYPE]: THEORY
BEGIN
IMPORTING relations_extra[D], relations_extra[R]
Drel: VAR pred[[D, D]]
Rrel: VAR pred[[R, R]]
d1, d2: VAR D
f: VAR (bijective?[D, R])
isomorphism?(Drel, Rrel)(f): bool =
FORALL d1, d2: Drel(d1, d2) IFF Rrel(f(d1), f(d2))
isomorphic?(Drel, Rrel): bool = EXISTS f: isomorphism?(Drel, Rrel)(f)
isomorphism_implication: LEMMA
FORALL Drel, Rrel, f:
trichotomous?(Drel) AND
irreflexive?(Rrel) AND
antisymmetric?(Rrel) AND preserves(f, Drel, Rrel)
IMPLIES isomorphism?(Drel, Rrel)(f)
isomorphism_preserves_reflexive: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(reflexive?[D](Drel) IFF reflexive?[R](Rrel))
isomorphism_preserves_irreflexive: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(irreflexive?[D](Drel) IFF irreflexive?[R](Rrel))
isomorphism_preserves_symmetric: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(symmetric?[D](Drel) IFF symmetric?[R](Rrel))
isomorphism_preserves_antisymmetric: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(antisymmetric?[D](Drel) IFF antisymmetric?[R](Rrel))
isomorphism_preserves_asymmetric: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(asymmetric?[D](Drel) IFF asymmetric?[R](Rrel))
% connected is the same as trichotomous
isomorphism_preserves_transitive: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(transitive?[D](Drel) IFF transitive?[R](Rrel))
isomorphism_preserves_dichotomous: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(dichotomous?[D](Drel) IFF dichotomous?[R](Rrel))
isomorphism_preserves_trichotomous: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(trichotomous?[D](Drel) IFF trichotomous?[R](Rrel))
isomorphism_preserves_well_founded: LEMMA
FORALL Drel, Rrel:
isomorphic?(Drel, Rrel) =>
(well_founded?[D](Drel) IFF well_founded?[R](Rrel))
isomorphism_inverse: LEMMA
FORALL Drel, Rrel, f:
isomorphism?(Drel, Rrel)(f) IFF
preserves(f, Drel, Rrel) AND preserves(inverse_alt(f), Rrel, Drel)
END isomorphism
¤ Dauer der Verarbeitung: 0.14 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.
|
