# HG changeset patch
# User huffman
# Date 1292783626 28800
# Node ID 752d81c2ce2596a128d60dd3dd59fdf203717955
# Parent  e9c9577d88b5f2a418690c74ef2b96e8da074047
add lemma u_map_oo

diff -r e9c9577d88b5 -r 752d81c2ce25 src/HOL/HOLCF/Map_Functions.thy
--- a/src/HOL/HOLCF/Map_Functions.thy	Sun Dec 19 09:52:33 2010 -0800
+++ b/src/HOL/HOLCF/Map_Functions.thy	Sun Dec 19 10:33:46 2010 -0800
@@ -191,6 +191,9 @@
 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"
 by (induct p) simp_all
 
+lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g"
+by (simp add: cfcomp1 u_map_map eta_cfun)
+
 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
 apply default
 apply (case_tac x, simp, simp add: ep_pair.e_inverse)