src/HOLCF/Up.thy
changeset 33587 54f98d225163
parent 33504 b4210cc3ac97
child 33808 31169fdc5ae7
     1.1 --- a/src/HOLCF/Up.thy	Mon Nov 09 15:29:58 2009 -0800
     1.2 +++ b/src/HOLCF/Up.thy	Mon Nov 09 15:51:32 2009 -0800
     1.3 @@ -303,6 +303,9 @@
     1.4  lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)"
     1.5  unfolding u_map_def by simp
     1.6  
     1.7 +lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p"
     1.8 +by (induct p) simp_all
     1.9 +
    1.10  lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
    1.11  apply default
    1.12  apply (case_tac x, simp, simp add: ep_pair.e_inverse)