src/HOLCF/Sprod.thy
changeset 35491 92e0028a46f2
parent 35115 446c5063e4fd
child 35525 fa231b86cb1e
     1.1 --- a/src/HOLCF/Sprod.thy	Mon Mar 01 16:58:16 2010 -0800
     1.2 +++ b/src/HOLCF/Sprod.thy	Mon Mar 01 17:32:23 2010 -0800
     1.3 @@ -245,6 +245,10 @@
     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_spair':
     1.8 +  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
     1.9 +by (cases "x = \<bottom> \<or> y = \<bottom>") auto
    1.10 +
    1.11  lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
    1.12  unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
    1.13