Quelle  isomorphism_equivalence.pvs

%-------------------------------------------------------------------------
%
%  Equivalence classes of automorphisms.
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[T], relations[pred[[T, T]]], relations[T]
%  orders: isomorphism[T,T], isomorphism_equivalence[T], relations_extra[T]
%
%-------------------------------------------------------------------------
isomorphism_equivalence[T: TYPE]: THEORY

EXPORTING ALL WITH orders[T], relations[pred[[T, T]]], relations[T],
     isomorphism[T, T], relations_extra[T]

 BEGIN

  IMPORTING function_inverse_def[T, T]      % Proofs only
  IMPORTING relations[pred[[T, T]]], isomorphism[T, T]

  isomorphism_reflexive: THEOREM reflexive?(isomorphic?)

  isomorphism_symmetric: THEOREM symmetric?(isomorphic?)

  isomorphism_transitive: THEOREM transitive?(isomorphic?)

  isomorphism_equivalence: JUDGEMENT
    isomorphic? HAS_TYPE equivalence[pred[[T, T]]]

 END isomorphism_equivalence