%-------------------------------------------------------------------------
%
%  Isomorphisms are symmetric.
%
%  For PVS version 3.2.  January 18, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[T1], orders[T2], relations[T1], relations[T2]
%  orders: isomorphism[T1,T2], isomorphism[T2,T1],
%    isomorphism_symmetric[T1,T2], relations_extra[T1], relations_extra[T2]
%
%-------------------------------------------------------------------------
isomorphism_symmetric[T1: TYPE, T2: TYPE]: THEORY

EXPORTING ALL WITH orders[T1], orders[T2], relations[T1], relations[T2],
     isomorphism[T1, T2], isomorphism[T2, T1],
     relations_extra[T1], relations_extra[T2]

 BEGIN

  IMPORTING function_inverse_def[T1, T2]  % Proofs only
  IMPORTING function_inverse_def[T2, T1]  % Proofs only
  IMPORTING isomorphism[T1, T2], isomorphism[T2, T1]

  rel1: VAR pred[[T1, T1]]
  rel2: VAR pred[[T2, T2]]

  isomorphism_symmetric: THEOREM
    FORALL rel1, rel2: isomorphic?(rel1, rel2) IFF isomorphic?(rel2, rel1)

 END isomorphism_symmetric