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