Added lift_map and subst_map.

--- a/src/HOL/Lambda/ListApplication.thy	Tue Jun 24 10:38:40 2003 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Tue Jun 24 10:39:14 2003 +0200
@@ -97,6 +97,17 @@
   apply simp
   done
 
+lemma lift_map [simp]:
+    "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
+  by (induct ts) simp_all
+
+lemma subst_map [simp]:
+    "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
+  by (induct ts) simp_all
+
+lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
+  by simp
+
 
 text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}