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