src/ZF/Resid/Substitution.thy

added ignored_consts, thms_containing, add_store_axioms(_i),
add_store_defs(_i), thms_of;
tuned pure thys;

(*  Title:      Substitution.thy
    ID:         $Id$
    Author:     Ole Rasmussen
    Copyright   1995  University of Cambridge
    Logic Image: ZF
*)

Substitution = SubUnion +

consts
  lift_rec      :: [i,i]=> i
  lift          :: i=>i
  subst_rec     :: [i,i,i]=> i
  "'/"          :: [i,i]=>i  (infixl 70)  (*subst*)
translations
  "lift(r)"  == "lift_rec(r,0)"
  "u/v" == "subst_rec(u,v,0)"
  
defs
  lift_rec_def  "lift_rec(r,kg) ==   
                     redex_rec(r,%i.(lam k:nat. if(i<k,Var(i),Var(succ(i)))), 
                                 %x m.(lam k:nat. Fun(m`(succ(k)))),   
                                 %b x y m p. lam k:nat. App(b,m`k,p`k))`kg"

  
(* subst_rec(u,Var(i),k)     = if k<i then Var(i-1)
                               else if k=i then u
                                    else Var(i)
   subst_rec(u,Fun(t),k)     = Fun(subst_rec(lift(u),t,succ(k)))
   subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))

*)
  subst_rec_def "subst_rec(u,t,kg) ==   
                     redex_rec(t,   
                       %i.(lam r:redexes. lam k:nat.   
                              if(k<i,Var(i#-1),   
                                if(k=i,r,Var(i)))),   
                       %x m.(lam r:redexes. lam k:nat.   
                             Fun(m`(lift(r))`(succ(k)))),   
                       %b x y m p. lam r:redexes. lam k:nat.   
                              App(b,m`r`k,p`r`k))`u`kg"


end