src/HOLCF/Sprod.thy
changeset 33808 31169fdc5ae7
parent 33587 54f98d225163
child 35115 446c5063e4fd
     1.1 --- a/src/HOLCF/Sprod.thy	Thu Nov 19 21:06:22 2009 -0800
     1.2 +++ b/src/HOLCF/Sprod.thy	Thu Nov 19 21:44:37 2009 -0800
     1.3 @@ -245,6 +245,9 @@
     1.4    "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
     1.5  by (simp add: sprod_map_def)
     1.6  
     1.7 +lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
     1.8 +unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
     1.9 +
    1.10  lemma sprod_map_map:
    1.11    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
    1.12      sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =