# HG changeset patch
# User huffman
# Date 1292092540 28800
# Node ID 32099ee71a2fcd44402ac82736b036022cb0e69b
# Parent  97bf008b9cfeb3c02f2d334161ca60e30bd10de9
new powerdomain lemmas

diff -r 97bf008b9cfe -r 32099ee71a2f src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Sat Dec 11 00:14:12 2010 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sat Dec 11 10:35:40 2010 -0800
@@ -400,6 +400,14 @@
   "convex_map\<cdot>f\<cdot>(convex_map\<cdot>g\<cdot>xs) = convex_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
 by (induct xs rule: convex_pd_induct, simp_all)
 
+lemma convex_bind_map:
+  "convex_bind\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>g = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))"
+by (simp add: convex_map_def convex_bind_bind)
+
+lemma convex_map_bind:
+  "convex_map\<cdot>f\<cdot>(convex_bind\<cdot>xs\<cdot>g) = convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_map\<cdot>f\<cdot>(g\<cdot>x))"
+by (simp add: convex_map_def convex_bind_bind)
+
 lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
 apply default
 apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
diff -r 97bf008b9cfe -r 32099ee71a2f src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Sat Dec 11 00:14:12 2010 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Sat Dec 11 10:35:40 2010 -0800
@@ -392,6 +392,14 @@
   "lower_map\<cdot>f\<cdot>(lower_map\<cdot>g\<cdot>xs) = lower_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
 by (induct xs rule: lower_pd_induct, simp_all)
 
+lemma lower_bind_map:
+  "lower_bind\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))"
+by (simp add: lower_map_def lower_bind_bind)
+
+lemma lower_map_bind:
+  "lower_map\<cdot>f\<cdot>(lower_bind\<cdot>xs\<cdot>g) = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_map\<cdot>f\<cdot>(g\<cdot>x))"
+by (simp add: lower_map_def lower_bind_bind)
+
 lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
 apply default
 apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
diff -r 97bf008b9cfe -r 32099ee71a2f src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Sat Dec 11 00:14:12 2010 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Sat Dec 11 10:35:40 2010 -0800
@@ -387,6 +387,14 @@
   "upper_map\<cdot>f\<cdot>(upper_map\<cdot>g\<cdot>xs) = upper_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>xs"
 by (induct xs rule: upper_pd_induct, simp_all)
 
+lemma upper_bind_map:
+  "upper_bind\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))"
+by (simp add: upper_map_def upper_bind_bind)
+
+lemma upper_map_bind:
+  "upper_map\<cdot>f\<cdot>(upper_bind\<cdot>xs\<cdot>g) = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_map\<cdot>f\<cdot>(g\<cdot>x))"
+by (simp add: upper_map_def upper_bind_bind)
+
 lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)"
 apply default
 apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)