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

relation_inverse_image[T, U: TYPE+]: THEORY
BEGIN
  
  R: VAR pred[[U, U]]
 
  f: VAR [T -> U]

  t: VAR T

  image_inverse(R, f):pred[[T, T]] = { (t1,t2:T) | R(f(t1),f(t2)) }

% The equivClass definition over the inverse image set
   equivClass(R, f, t):pred[T] = { t1:T | image_inverse(R, f)(t, t1) }
 
% Curried form
  image_inverse(R)(f):pred[[T, T]] = image_inverse(R, f)

% Curried form
  equivClass(R, f)(t):pred[T] =  equivClass(R, f, t)

  equivClass_is_nonempty: LEMMA equivalence?[U](R)
    IMPLIES nonempty?[T](equivClass(R,f)(t))

  equivClass_equal_is_nonempty: LEMMA nonempty?[T](equivClass(=, f)(t))

  inverse_image_of_equivalence: LEMMA equivalence?[U](R) 
    IMPLIES equivalence?[T](image_inverse(R, f))

  preserves_eqv_of_inv_image: LEMMA EXISTS R: equivalence?[T](image_inverse(R, f))  

  inverse_image_of_equality: LEMMA equivalence?[T](image_inverse(=, f))
  
  image_inverse_eq_is_eq_kernel: LEMMA 
    EquivalenceKernel[T, T, U](f) = image_inverse(=)(f)
     
  inv_img_surj_impl_codom_eq: LEMMA  
    FORALL (f:(surjective?[T, U])):
      equivalence?[T](image_inverse(R,f)) IMPLIES equivalence?[U](R)

  right_inv_inv_finv_image_impl_codom_eq: LEMMA  
    right_inverse?(inverse(f), f) IMPLIES
      equivalence?[T](image_inverse(R, f)) IMPLIES equivalence?[U](R)

  surjective_eqv_image_inv_rel_codomain: THEOREM 
    FORALL (f:(surjective?[T, U])):
      equivalence?[T](image_inverse(R)(f)) = equivalence?[U](R)

  right_inv_inv_finv_image_eq_codom_eq: LEMMA  
    right_inverse?(inverse(f), f) IMPLIES
      equivalence?[T](image_inverse(R, f)) =  equivalence?[U](R)

END relation_inverse_image