# HG changeset patch
# User huffman
# Date 1267493543 28800
# Node ID 92e0028a46f2dca8433ab88bee41ce728df4a434
# Parent  63f8121c6585366e978de223342da8f79d4be879
add lemmas about ssum_map and sprod_map

diff -r 63f8121c6585 -r 92e0028a46f2 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Mon Mar 01 16:58:16 2010 -0800
+++ b/src/HOLCF/Sprod.thy	Mon Mar 01 17:32:23 2010 -0800
@@ -245,6 +245,10 @@
   "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)"
 by (simp add: sprod_map_def)
 
+lemma sprod_map_spair':
+  "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:)"
+by (cases "x = \<bottom> \<or> y = \<bottom>") auto
+
 lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
 unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
 
diff -r 63f8121c6585 -r 92e0028a46f2 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Mon Mar 01 16:58:16 2010 -0800
+++ b/src/HOLCF/Ssum.thy	Mon Mar 01 17:32:23 2010 -0800
@@ -226,6 +226,12 @@
 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_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)"
+by (cases "x = \<bottom>") simp_all
+
+lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)"
+by (cases "x = \<bottom>") simp_all
+
 lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID"
 unfolding ssum_map_def by (simp add: expand_cfun_eq eta_cfun)