9284
|
1 |
(* Title: ZF/Resid/Substitution.thy
|
1048
|
2 |
ID: $Id$
|
1478
|
3 |
Author: Ole Rasmussen
|
1048
|
4 |
Copyright 1995 University of Cambridge
|
|
5 |
Logic Image: ZF
|
|
6 |
*)
|
|
7 |
|
6046
|
8 |
Substitution = Redex +
|
1048
|
9 |
|
|
10 |
consts
|
6046
|
11 |
lift_aux :: i=> i
|
|
12 |
lift :: i=> i
|
|
13 |
subst_aux :: i=> i
|
|
14 |
"'/" :: [i,i]=>i (infixl 70) (*subst*)
|
|
15 |
|
|
16 |
constdefs
|
1478
|
17 |
lift_rec :: [i,i]=> i
|
6046
|
18 |
"lift_rec(r,k) == lift_aux(r)`k"
|
|
19 |
|
6068
|
20 |
subst_rec :: [i,i,i]=> i (**NOTE THE ARGUMENT ORDER BELOW**)
|
6046
|
21 |
"subst_rec(u,r,k) == subst_aux(r)`u`k"
|
|
22 |
|
1048
|
23 |
translations
|
|
24 |
"lift(r)" == "lift_rec(r,0)"
|
6046
|
25 |
"u/v" == "subst_rec(u,v,0)"
|
1048
|
26 |
|
6046
|
27 |
|
|
28 |
(** The clumsy _aux functions are required because other arguments vary
|
|
29 |
in the recursive calls ***)
|
|
30 |
|
|
31 |
primrec
|
11319
|
32 |
"lift_aux(Var(i)) = (\\<lambda>k \\<in> nat. if i<k then Var(i) else Var(succ(i)))"
|
6046
|
33 |
|
11319
|
34 |
"lift_aux(Fun(t)) = (\\<lambda>k \\<in> nat. Fun(lift_aux(t) ` succ(k)))"
|
6046
|
35 |
|
11319
|
36 |
"lift_aux(App(b,f,a)) = (\\<lambda>k \\<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
|
6046
|
37 |
|
1048
|
38 |
|
|
39 |
|
6046
|
40 |
primrec
|
|
41 |
"subst_aux(Var(i)) =
|
11319
|
42 |
(\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. if k<i then Var(i #- 1)
|
6068
|
43 |
else if k=i then r else Var(i))"
|
6046
|
44 |
"subst_aux(Fun(t)) =
|
11319
|
45 |
(\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
|
6046
|
46 |
|
|
47 |
"subst_aux(App(b,f,a)) =
|
11319
|
48 |
(\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
|
1048
|
49 |
|
|
50 |
end
|
|
51 |
|
|
52 |
|