src/HOLCF/Ssum.thy
changeset 33808 31169fdc5ae7
parent 33587 54f98d225163
child 35427 ad039d29e01c
child 35491 92e0028a46f2
--- a/src/HOLCF/Ssum.thy	Thu Nov 19 21:06:22 2009 -0800
+++ b/src/HOLCF/Ssum.thy	Thu Nov 19 21:44:37 2009 -0800
@@ -226,6 +226,9 @@
 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
 unfolding ssum_map_def by simp
 
+lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
+unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)
+
 lemma ssum_map_map:
   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
     ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =