Quelle  similarity.pvs   Sprache: PVS

%-------------------------------------------------------------------------
%
%  Similar ordered sets.  Two totally ordered sets are similar if there
%  exists an bijective function from the first to the second that
%  preserves ordering.  This is a special case of isomorphism.
%
%  For PVS version 3.2.  March 5, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[D], orders[R]
%  orders: isomorphism[D,R], similarity[D,R]
%
%-------------------------------------------------------------------------
similarity[D: TYPE, R: TYPE]: THEORY
 BEGIN

  IMPORTING isomorphism[D, R]

  Dord: VAR (total_order?[D])
  Rord: VAR (total_order?[R])
  f: VAR (bijective?[D, R])

  similarity?(Dord, Rord)(f): bool = preserves(f, Dord, Rord)

  similar?(Dord, Rord): bool = EXISTS f: similarity?(Dord, Rord)(f)

  similarity_is_isomorphism: LEMMA
    FORALL Dord, Rord, f:
      similarity?(Dord, Rord)(f) IMPLIES isomorphism?(Dord, Rord)(f)

  similar_is_isomorphic: COROLLARY
    FORALL Dord, Rord: similar?(Dord, Rord) IMPLIES isomorphic?(Dord, Rord)

 END similarity