src/ZF/Resid/Substitution.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 3840 e0baea4d485a permissions -rw-r--r--
expanded tabs
```     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
```