%--------------------------------------------------------------%
%   Author: Dragan Stosic                                      %
%--------------------------------------------------------------%

relation_inverse_extension[T, U: TYPE+]: THEORY
BEGIN

 IMPORTING relation_inverse_image[T, U],
           relation_inverse_image[U, T],
           relation_extension[T, U]

 f: VAR [T -> U]

 g: VAR [U -> T]

 m, n :VAR [T, U]

 re_U: VAR equivalence[U]

 re_T: VAR equivalence[T]

 l_T(re_U, f):pred[[T, T]] = image_inverse(re_U, f)

 le_U_induces_equivalence :JUDGEMENT l_T(re_U, f) HAS_TYPE equivalence[T]
  
 l_U(re_T, g):pred[[U, U]] = image_inverse(re_T, g)

 le_T_induces_equivalence: JUDGEMENT l_U(re_T, g) HAS_TYPE equivalence[U]

% etended equivalence relation based on inverse images of equivalence 
% relations

 rel_inv_extension(re_T, re_U, f, g) : set[[[T, U], [T, U]]] =
   { (m, n) | l_T(re_U, f)(n`1,m`1) AND l_U(re_T, g)(n`2,m`2) }

 rel_inv_extension_is_equivalence: JUDGEMENT 
   rel_inv_extension(re_T, re_U, f, g) HAS_TYPE equivalence[[T, U]]

% connection between two relations: 
% rel_extension and rel_image_extension

 rel_extension_IFF_rel_ext : LEMMA 
   LET GFm=(g(m`2),f(m`1)), GFn=(g(n`2),f(n`1)) IN
     rel_extension(re_T, re_U)(GFm, GFn) = 
       rel_inv_extension(re_T, re_U, f, g)(n, m)

% replaced: definition of the rel_inv_extension using the rel_extension 

 rel_inv_extension2(re_T, re_U, f, g):set[[[T, U], [T, U]]] = 
   { (n, m) | LET GFm=(g(m`2),f(m`1)), GFn=(g(n`2),f(n`1)) IN
      rel_extension(re_T, re_U)(GFm, GFn) 
   }

 rel_inv_extension2_is_equivalence: JUDGEMENT 
   rel_inv_extension2(re_T, re_U, f, g) HAS_TYPE equivalence[[T, U]]

END relation_inverse_extension