# 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)