src/HOLCF/ConvexPD.thy

 
 lemma convex_map_plus [simp]:
   "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
 unfolding convex_map_def by simp
 
+lemma convex_map_bottom [simp]: "convex_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<natural>"
+unfolding convex_map_def by simp
+
 lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
 by (induct xs rule: convex_pd_induct, simp_all)
 
 lemma convex_map_ID: "convex_map\<cdot>ID = ID"
 by (simp add: cfun_eq_iff ID_def convex_map_ident)

 
 lemma convex_join_plus [simp]:
   "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
 unfolding convex_join_def by simp
 
+lemma convex_join_bottom [simp]: "convex_join\<cdot>\<bottom> = \<bottom>"
+unfolding convex_join_def by simp
+
 lemma convex_join_map_unit:
   "convex_join\<cdot>(convex_map\<cdot>convex_unit\<cdot>xs) = xs"
 by (induct xs rule: convex_pd_induct, simp_all)
 
 lemma convex_join_map_join: