|
1478
|
1 |
(* Title: Substitution.thy
|
|
1048
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Ole Rasmussen
|
|
1048
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
Logic Image: ZF
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
Substitution = SubUnion +
|
|
|
9 |
|
|
|
10 |
consts
|
|
1478
|
11 |
lift_rec :: [i,i]=> i
|
|
|
12 |
lift :: i=>i
|
|
|
13 |
subst_rec :: [i,i,i]=> i
|
|
1401
|
14 |
"'/" :: [i,i]=>i (infixl 70) (*subst*)
|
|
1048
|
15 |
translations
|
|
|
16 |
"lift(r)" == "lift_rec(r,0)"
|
|
|
17 |
"u/v" == "subst_rec(u,v,0)"
|
|
|
18 |
|
|
|
19 |
defs
|
|
1478
|
20 |
lift_rec_def "lift_rec(r,kg) ==
|
|
3840
|
21 |
redex_rec(r,%i.(lam k:nat. if(i<k,Var(i),Var(succ(i)))),
|
|
|
22 |
%x m.(lam k:nat. Fun(m`(succ(k)))),
|
|
|
23 |
%b x y m p. lam k:nat. App(b,m`k,p`k))`kg"
|
|
1048
|
24 |
|
|
|
25 |
|
|
|
26 |
(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
|
|
|
27 |
else if k=i then u
|
|
|
28 |
else Var(i)
|
|
|
29 |
subst_rec(u,Fun(t),k) = Fun(subst_rec(lift(u),t,succ(k)))
|
|
|
30 |
subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
|
|
|
31 |
|
|
|
32 |
*)
|
|
1478
|
33 |
subst_rec_def "subst_rec(u,t,kg) ==
|
|
|
34 |
redex_rec(t,
|
|
3840
|
35 |
%i.(lam r:redexes. lam k:nat.
|
|
1478
|
36 |
if(k<i,Var(i#-1),
|
|
|
37 |
if(k=i,r,Var(i)))),
|
|
3840
|
38 |
%x m.(lam r:redexes. lam k:nat.
|
|
1155
|
39 |
Fun(m`(lift(r))`(succ(k)))),
|
|
3840
|
40 |
%b x y m p. lam r:redexes. lam k:nat.
|
|
1478
|
41 |
App(b,m`r`k,p`r`k))`u`kg"
|
|
1048
|
42 |
|
|
|
43 |
|
|
|
44 |
end
|
|
|
45 |
|
|
|
46 |
|