# HG changeset patch
# User berghofe
# Date 1056443954 -7200
# Node ID fe45b97b62ea4509d7dae5e210c95b4bf9baa49d
# Parent  8abaf978c9c21a465abeeee35d15ddcb98f13004
Added lift_map and subst_map.

diff -r 8abaf978c9c2 -r fe45b97b62ea src/HOL/Lambda/ListApplication.thy
--- 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>"}. *}