author | wenzelm |
Tue, 20 Oct 1998 16:26:20 +0200 | |
changeset 5686 | 1f053d05f571 |
parent 5514 | 324e1560a5c9 |
child 6046 | 2c8a8be36c94 |
permissions | -rw-r--r-- |
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. |
5514
324e1560a5c9
inserted space in #-1 to prevent confusion with an integer constant
paulson
parents:
3840
diff
changeset
|
36 |
if(k<i,Var(i #- 1), |
1478 | 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 |