--- a/src/HOLCF/ConvexPD.thy Tue Nov 16 12:08:28 2010 -0800
+++ b/src/HOLCF/ConvexPD.thy Tue Nov 16 13:37:17 2010 -0800
@@ -360,6 +360,11 @@
lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
+lemma convex_bind_bind:
+ "convex_bind\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>g =
+ convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}
--- a/src/HOLCF/LowerPD.thy Tue Nov 16 12:08:28 2010 -0800
+++ b/src/HOLCF/LowerPD.thy Tue Nov 16 13:37:17 2010 -0800
@@ -353,6 +353,10 @@
lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)
+lemma lower_bind_bind:
+ "lower_bind\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>g = lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}
--- a/src/HOLCF/UpperPD.thy Tue Nov 16 12:08:28 2010 -0800
+++ b/src/HOLCF/UpperPD.thy Tue Nov 16 13:37:17 2010 -0800
@@ -348,6 +348,10 @@
lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)
+lemma upper_bind_bind:
+ "upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct xs, simp_all)
+
subsection {* Map *}