--- 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>"}. *}