fundamental theorems on Set.bind

--- a/src/HOL/Complete_Lattices.thy	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/Complete_Lattices.thy	Thu Dec 29 14:23:40 2011 +0100
@@ -928,11 +928,15 @@
   "Set.bind A f = UNION A f"
   by (simp add: bind_def UNION_eq)
 
+lemma member_bind [simp]:
+  "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
+  by (simp add: bind_UNION)
+
 lemma Union_image_eq [simp]:
   "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   by (rule sym) (fact SUP_def)
 
-lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
+lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
   by (auto simp add: SUP_def image_def)
 
 lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"

--- 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 *}