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 lift db |
21 primrec lift db |
22 lift_Var "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(Suc i))" |
23 lift_App "lift (s @ t) k = (lift s k) @ (lift t k)" |
23 "lift (s @ t) k = (lift s k) @ (lift t k)" |
24 lift_Fun "lift (Fun s) k = Fun(lift s (Suc k))" |
24 "lift (Fun s) k = Fun(lift s (Suc k))" |
25 |
25 |
26 primrec subst db |
26 primrec subst db |
27 subst_Var "(Var i)[s/k] = (if k < i then Var(pred i) |
27 subst_Var "(Var i)[s/k] = (if k < i then Var(pred i) |
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_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])" |
30 subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])" |
31 |
31 |
32 primrec liftn db |
32 primrec liftn db |
33 liftn_Var "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_App "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_Fun "liftn n (Fun s) k = Fun(liftn n s (Suc k))" |
35 "liftn n (Fun s) k = Fun(liftn n s (Suc k))" |
36 |
36 |
37 primrec substn db |
37 primrec substn db |
38 substn_Var "substn (Var i) s k = (if k < i then Var(pred i) |
38 "substn (Var i) s k = (if k < i then Var(pred i) |
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_App "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_Fun "substn (Fun t) s k = Fun (substn t s (Suc k))" |
41 "substn (Fun t) s k = Fun (substn t s (Suc k))" |
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 |