%%-------------------** Abstract Reduction System (ARS) **-------------------
%%                                                                          
%% Authors         : Andre Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%
%%                         and 
%%
%%                   Mauricio Ayala Rincon  
%%                   Universidade de Brasília - Brasil  
%%              
%% Last Modified On: December 02, 2006                                      
%%                                                                          
%%---------------------------------------------------------------------------


%%---------------------------------------------------------------------------
%%
%% We defined reflexive, symmetric, transitive, reflexive and transitive, 
%% and equivalence closures of a binary relation in the same way that 
%% Alfons Geser defined in .../lib/../closure_ops.pvs. We just changed
%% the names of the definitions and we proved some additional properties.
%%                                                                          
%%---------------------------------------------------------------------------



relations_closure[T : TYPE] : THEORY
BEGIN


 IMPORTING
    orders@closure_ops[T],
    sets_lemmas[T]

   S, R: VAR pred[[T, T]]
   n: VAR nat
   p: VAR posnat


   reflexive: TYPE = (reflexive?)

   symmetric: TYPE = (symmetric?)

   transitive: TYPE = (transitive?)

   reflexive_transitive?(R): bool = reflexive?(R) & transitive?(R)

   reflexive_transitive: TYPE = (reflexive_transitive?)

   equivalence: TYPE = (equivalence?)



% % Reflexive Closure (RC)

    RC(R): reflexive = union(R, =)


% %% Properties

   change_to_RC : LEMMA reflexive_closure(R) = RC(R) 

   R_subset_RC : LEMMA subset?(R, RC(R))

   RC_idempotent : LEMMA  RC(RC(R)) = RC(R)

   RC_characterization : LEMMA  reflexive?(S) <=> (S = RC(S))



% % Symmetric Closure (SC)

    SC(R): symmetric = union(R, converse(R))


% %% Properties

   change_to_SC : LEMMA symmetric_closure(R) = SC(R)

   R_subset_SC : LEMMA subset?(R, SC(R))

   SC_idempotent : LEMMA  SC(SC(R)) = SC(R)

   SC_characterization : LEMMA  symmetric?(S) <=> (S = SC(S))

 

% % Transitive Closure (TC)

    TC(R): transitive = IUnion(LAMBDA p: iterate(R, p))


% %% Properties

   change_to_TC : LEMMA transitive_closure(R) = TC(R)

   R_subset_TC :LEMMA subset?(R, TC(R))

   TC_converse: LEMMA  TC(converse(R)) = converse(TC(R))

   TC_idempotent : LEMMA  TC(TC(R)) = TC(R)

   TC_characterization : LEMMA  transitive?(S) <=> (S = TC(S))

   

% % Reflexive Transitive Closure (RTC)

   RTC(R): reflexive_transitive = IUnion(LAMBDA n: iterate(R, n)) 


% %% Properties

   change_to_RTC : LEMMA preorder_closure(R) = RTC(R)

   R_subset_RTC: LEMMA subset?(R, RTC(R))

   iterate_RTC: LEMMA FORALL n : subset?(iterate(R, n), RTC(R))

   RTC_idempotent : LEMMA  RTC(RTC(R)) = RTC(R)

   RTC_characterization : LEMMA reflexive_transitive?(S) <=> (S = RTC(S))



% % Equivalence Closure (EC)

    EC(R): equivalence = RTC(SC(R))


% %% Properties

    change_to_EC : LEMMA equivalence_closure(R) = EC(R)  

    R_subset_EC: LEMMA subset?(R, EC(R))

    RTC_subset_EC: LEMMA subset?(RTC(R), EC(R))

    EC_idempotent : LEMMA  EC(EC(R)) = EC(R)

    EC_characterization : LEMMA  equivalence?(S) <=> (S = EC(S))


END relations_closure