# HG changeset patch
# User huffman
# Date 1289938108 28800
# Node ID 5c6225a1c2c040493cbb6bbec4e4bc0fbe153de9
# Parent  fa5e0cacd5e712ad8f2dda336a52dbe308c4ec7e
add lemmas about powerdomains

diff -r fa5e0cacd5e7 -r 5c6225a1c2c0 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Tue Nov 16 11:57:10 2010 -0800
+++ b/src/HOLCF/ConvexPD.thy	Tue Nov 16 12:08:28 2010 -0800
@@ -375,6 +375,9 @@
   "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)
 
@@ -517,6 +520,9 @@
   "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)
diff -r fa5e0cacd5e7 -r 5c6225a1c2c0 src/HOLCF/LowerPD.thy
--- 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)
diff -r fa5e0cacd5e7 -r 5c6225a1c2c0 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Tue Nov 16 11:57:10 2010 -0800
+++ b/src/HOLCF/UpperPD.thy	Tue Nov 16 12:08:28 2010 -0800
@@ -363,6 +363,9 @@
   "upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
 unfolding upper_map_def by simp
 
+lemma upper_map_bottom [simp]: "upper_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<sharp>"
+unfolding upper_map_def by simp
+
 lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
 by (induct xs rule: upper_pd_induct, simp_all)
 
@@ -503,6 +506,9 @@
   "upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
 unfolding upper_join_def by simp
 
+lemma upper_join_bottom [simp]: "upper_join\<cdot>\<bottom> = \<bottom>"
+unfolding upper_join_def by simp
+
 lemma upper_join_map_unit:
   "upper_join\<cdot>(upper_map\<cdot>upper_unit\<cdot>xs) = xs"
 by (induct xs rule: upper_pd_induct, simp_all)