|
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 |