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