Quelle isomorphism.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
%  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 (jamesj@acm.org), 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

quality93%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.