# HG changeset patch
# User huffman
# Date 1289943437 28800
# Node ID 0e77e45d2ffc489723107ab57dd3fc05827fdb2e
# Parent  5c6225a1c2c040493cbb6bbec4e4bc0fbe153de9
add bind_bind rules for powerdomains

diff -r 5c6225a1c2c0 -r 0e77e45d2ffc src/HOLCF/ConvexPD.thy
--- 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 *}
 
diff -r 5c6225a1c2c0 -r 0e77e45d2ffc src/HOLCF/LowerPD.thy
--- 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 *}
 
diff -r 5c6225a1c2c0 -r 0e77e45d2ffc src/HOLCF/UpperPD.thy
--- 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 *}