diff -r 313be214e40a -r 6a86cc88b02f src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/Set.thy	Thu Dec 29 14:23:40 2011 +0100
@@ -1790,6 +1790,22 @@
 
 hide_const (open) bind
 
+lemma bind_bind:
+  fixes A :: "'a set"
+  shows "Set.bind (Set.bind A B) C = Set.bind A (\<lambda>x. Set.bind (B x) C)"
+  by (auto simp add: bind_def)
+
+lemma empty_bind [simp]:
+  "Set.bind {} B = {}"
+  by (simp add: bind_def)
+
+lemma nonempty_bind_const:
+  "A \<noteq> {} \<Longrightarrow> Set.bind A (\<lambda>_. B) = B"
+  by (auto simp add: bind_def)
+
+lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
+  by (auto simp add: bind_def)
+
 
 subsubsection {* Operations for execution *}