src/ZF/Resid/Substitution.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
lcp@1048
     1
(*  Title: 	Substitution.thy
lcp@1048
     2
    ID:         $Id$
lcp@1048
     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@1401
    11
  lift_rec	:: [i,i]=> i
clasohm@1401
    12
  lift		:: i=>i
clasohm@1401
    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@1155
    20
  lift_rec_def	"lift_rec(r,kg) ==   
clasohm@1155
    21
		     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), 
clasohm@1155
    22
		                 %x m.(lam k:nat.Fun(m`(succ(k)))),   
clasohm@1155
    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@1155
    33
  subst_rec_def	"subst_rec(u,t,kg) ==   
clasohm@1155
    34
		     redex_rec(t,   
clasohm@1155
    35
		       %i.(lam r:redexes.lam k:nat.   
clasohm@1155
    36
		              if(k<i,Var(i#-1),   
clasohm@1155
    37
		                if(k=i,r,Var(i)))),   
clasohm@1155
    38
		       %x m.(lam r:redexes.lam k:nat.   
clasohm@1155
    39
                             Fun(m`(lift(r))`(succ(k)))),   
clasohm@1155
    40
		       %b x y m p.lam r:redexes.lam k:nat.   
clasohm@1155
    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