Added lift_map and subst_map.
authorberghofe
Tue Jun 24 10:39:14 2003 +0200 (2003-06-24)
changeset 14066fe45b97b62ea
parent 14065 8abaf978c9c2
child 14067 3cc65d66fa12
Added lift_map and subst_map.
src/HOL/Lambda/ListApplication.thy
     1.1 --- a/src/HOL/Lambda/ListApplication.thy	Tue Jun 24 10:38:40 2003 +0200
     1.2 +++ b/src/HOL/Lambda/ListApplication.thy	Tue Jun 24 10:39:14 2003 +0200
     1.3 @@ -97,6 +97,17 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 +lemma lift_map [simp]:
     1.8 +    "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
     1.9 +  by (induct ts) simp_all
    1.10 +
    1.11 +lemma subst_map [simp]:
    1.12 +    "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
    1.13 +  by (induct ts) simp_all
    1.14 +
    1.15 +lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
    1.16 +  by simp
    1.17 +
    1.18  
    1.19  text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
    1.20