17 (* optimized versions *) |
17 (* optimized versions *) |
18 substn :: [dB,dB,nat] => dB |
18 substn :: [dB,dB,nat] => dB |
19 liftn :: [nat,dB,nat] => dB |
19 liftn :: [nat,dB,nat] => dB |
20 |
20 |
21 primrec |
21 primrec |
22 "lift (Var i) k = (if i < k then Var i else Var(Suc i))" |
22 "lift (Var i) k = (if i < k then Var i else Var(i+1))" |
23 "lift (s $ t) k = (lift s k) $ (lift t k)" |
23 "lift (s $ t) k = (lift s k) $ (lift t k)" |
24 "lift (Abs s) k = Abs(lift s (Suc k))" |
24 "lift (Abs s) k = Abs(lift s (k+1))" |
25 |
25 |
26 primrec |
26 primrec |
27 subst_Var "(Var i)[s/k] = (if k < i then Var(i-1) |
27 subst_Var "(Var i)[s/k] = (if k < i then Var(i-1) |
28 else if i = k then s else Var i)" |
28 else if i = k then s else Var i)" |
29 subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]" |
29 subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]" |
30 subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])" |
30 subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])" |
31 |
31 |
32 primrec |
32 primrec |
33 "liftn n (Var i) k = (if i < k then Var i else Var(i+n))" |
33 "liftn n (Var i) k = (if i < k then Var i else Var(i+n))" |
34 "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)" |
34 "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)" |
35 "liftn n (Abs s) k = Abs(liftn n s (Suc k))" |
35 "liftn n (Abs s) k = Abs(liftn n s (k+1))" |
36 |
36 |
37 primrec |
37 primrec |
38 "substn (Var i) s k = (if k < i then Var(i-1) |
38 "substn (Var i) s k = (if k < i then Var(i-1) |
39 else if i = k then liftn k s 0 else Var i)" |
39 else if i = k then liftn k s 0 else Var i)" |
40 "substn (t $ u) s k = (substn t s k) $ (substn u s k)" |
40 "substn (t $ u) s k = (substn t s k) $ (substn u s k)" |
41 "substn (Abs t) s k = Abs (substn t s (Suc k))" |
41 "substn (Abs t) s k = Abs (substn t s (k+1))" |
42 |
42 |
43 consts beta :: "(dB * dB) set" |
43 consts beta :: "(dB * dB) set" |
44 |
44 |
45 syntax "->", "->>" :: [dB,dB] => bool (infixl 50) |
45 syntax "->", "->>" :: [dB,dB] => bool (infixl 50) |
46 |
46 |