--- a/src/HOLCF/LowerPD.thy Tue Nov 16 11:57:10 2010 -0800
+++ b/src/HOLCF/LowerPD.thy Tue Nov 16 12:08:28 2010 -0800
@@ -368,6 +368,9 @@
"lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
unfolding lower_map_def by simp
+lemma lower_map_bottom [simp]: "lower_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<flat>"
+unfolding lower_map_def by simp
+
lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
by (induct xs rule: lower_pd_induct, simp_all)
@@ -508,6 +511,9 @@
"lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
unfolding lower_join_def by simp
+lemma lower_join_bottom [simp]: "lower_join\<cdot>\<bottom> = \<bottom>"
+unfolding lower_join_def by simp
+
lemma lower_join_map_unit:
"lower_join\<cdot>(lower_map\<cdot>lower_unit\<cdot>xs) = xs"
by (induct xs rule: lower_pd_induct, simp_all)