--- a/src/HOL/Lambda/Lambda.thy Thu Jun 22 12:44:29 1995 +0200
+++ b/src/HOL/Lambda/Lambda.thy Thu Jun 22 12:45:08 1995 +0200
@@ -14,17 +14,31 @@
consts
subst :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
lift :: "[db,nat] => db"
+ (* optimized versions *)
+ substn :: "[db,db,nat] => db"
+ liftn :: "[nat,db,nat] => db"
+
+primrec lift db
+ lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
+ lift_App "lift (s @ t) k = (lift s k) @ (lift t k)"
+ lift_Fun "lift (Fun s) k = Fun(lift s (Suc k))"
primrec subst db
- subst_Var "(Var i)[s/n] = (if n < i then Var(pred i)
- else if i = n then s else Var i)"
- subst_App "(t @ u)[s/n] = t[s/n] @ u[s/n]"
- subst_Fun "(Fun t)[s/n] = Fun (t[lift s 0 / Suc n])"
+ subst_Var "(Var i)[s/k] = (if k < i then Var(pred i)
+ else if i = k then s else Var i)"
+ subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
+ subst_Fun "(Fun t)[s/k] = Fun (t[lift s 0 / Suc k])"
-primrec lift db
- lift_Var "lift (Var i) n = (if i < n then Var i else Var(Suc i))"
- lift_App "lift (s @ t) n = (lift s n) @ (lift t n)"
- lift_Fun "lift (Fun s) n = Fun(lift s (Suc n))"
+primrec liftn db
+ liftn_Var "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
+ liftn_App "liftn n (s @ t) k = (liftn n s k) @ (liftn n t k)"
+ liftn_Fun "liftn n (Fun s) k = Fun(liftn n s (Suc k))"
+
+primrec substn db
+ substn_Var "substn (Var i) s k = (if k < i then Var(pred i)
+ else if i = k then liftn k s 0 else Var i)"
+ substn_App "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
+ substn_Fun "substn (Fun t) s k = Fun (substn t s (Suc k))"
consts beta :: "(db * db) set"