--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Resid/Substitution.thy Thu Apr 13 15:38:07 1995 +0200
@@ -0,0 +1,46 @@
+(* 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
+
+