Quelle  replacement.pvs

%%-------------------** Term Rewriting System (TRS) **------------------------
%%                                                                          
%% Authors         : Andre Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%
%%                         and 
%%
%%                   Mauricio Ayala Rincon  
%%                   Universidade de Brasília - Brasil  
%%              
%% Last Modified On: September 29, 2009                                      
%%                                                                          
%%----------------------------------------------------------------------------


 replacement[variable: TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY
  BEGIN
    
   IMPORTING subterm[variable,symbol, arity]
  

  p, q, p1, p2, q1: VAR position
           s, r, t: VAR term
                 i: VAR posnat
                fs: VAR finseq[term]
              x, y: VAR (V)


%%%% Definition: replacing the subterm of s at position p by t %%%%%%%%%%%%%%%

 replaceTerm(s: term, t: term, (p: positions?(s))): RECURSIVE term =
     (IF length(p) = 0
      THEN
        t
      ELSE
        LET st = args(s),
             i = first(p),
             q = rest(p),
           rst = replace(replaceTerm(st(i-1), t, q), st,i-1) IN
        app(f(s), rst)
      ENDIF)
   MEASURE length(p)


%%%% Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 
 replace_preserv_pos: LEMMA positionsOF(s)(p) 
                            => 
                             positionsOF(replaceTerm(s, t, p))(p)


 replace_compose_pos: LEMMA positionsOF(t)(q) & positionsOF(s)(p)
                              =>
                                positionsOF(replaceTerm(s, t, p))(p o q)


 replace_preserv_parallel_pos: LEMMA positionsOF(s)(q) & 
                                     positionsOF(s)(p) & 
                                     parallel(p, q)
                                        =>
                                          positionsOF(replaceTerm(s, t, p))(q)


 preserv_unchanged_pos: LEMMA positionsOF(s)(p) & 
                     positionsOF(replaceTerm(s, t, p))(q) & 
                     parallel(p, q)  
                          => positionsOF(s)(q)


 subterm_of_replace: LEMMA positionsOF(s)(p) 
                              => 
                                subtermOF(replaceTerm(s, t, p),p) = t


 replace_subterm_of_term: LEMMA positionsOF(s)(p)
                                    => 
                                     replaceTerm(s, subtermOF(s, p), p) = s


 replace_embedding: LEMMA positionsOF(s)(p) & positionsOF(t)(q) =>
                    subtermOF(replaceTerm(s, t, p),p o q) = subtermOF(t, q)


 replace_associativity: LEMMA positionsOF(s)(p) & positionsOF(t)(q) =>
  replaceTerm(replaceTerm(s,t,p),r,p o q) = replaceTerm(s,replaceTerm(t,r,q),p)


 replace_distributivity: LEMMA positionsOF(s)(p o q) =>
   subtermOF(replaceTerm(s,t,p o q), p) = replaceTerm(subtermOF(s, p), t, q)


 replace_dominance: LEMMA positionsOF(s)(p o q) =>
                replaceTerm(replaceTerm(s,t,p o q),r,p) = replaceTerm(s,r,p)


 replace_persistence: LEMMA positionsOF(s)(p) & 
                            positionsOF(s)(q) & 
                            parallel(p,q)
                             =>
                              subtermOF(replaceTerm(s, t, p), q) = subtermOF(s,q)


 replace_commutativity: LEMMA 
   positionsOF(s)(p) & positionsOF(s)(q) & parallel(p,q) 
     =>
      replaceTerm(replaceTerm(s,t,p),r,q) = replaceTerm(replaceTerm(s,r,q),t,p)


 pos_replaces_is_subset: LEMMA
       FORALL t, x, (p: positions?(t)): 
           subset?(positionsOF(replaceTerm(t, x, p)), positionsOF(t))


 pos_occ_var_replace: LEMMA
     FORALL t, y, x, (p: positions?(t)): 
           Pos_var(t, x)(p) & y /= x
             =>  Pos_var(replaceTerm(t, y, p), x) = remove(p, Pos_var(t, x))


  pos_occ_var_replace_as_diff: LEMMA
   FORALL t, y, x, (p: positions?(t)): 
    Pos_var(t, x)(p) & y /= x
    =>  
     Pos_var(replaceTerm(t, y, p), x) = difference(Pos_var(t, x), singleton(p))


END replacement