--- a/src/ZF/Resid/Substitution.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Substitution.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Substitution.thy
+(* Title: Substitution.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -8,19 +8,19 @@
Substitution = SubUnion +
consts
- lift_rec :: [i,i]=> i
- lift :: i=>i
- subst_rec :: [i,i,i]=> i
+ 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"
+ 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)
@@ -30,15 +30,15 @@
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.
+ 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"
+ %b x y m p.lam r:redexes.lam k:nat.
+ App(b,m`r`k,p`r`k))`u`kg"
end