author haftmann Thu, 29 Dec 2011 14:23:40 +0100 changeset 46036 6a86cc88b02f parent 46035 313be214e40a child 46037 49a436ada6a2
fundamental theorems on Set.bind
 src/HOL/Complete_Lattices.thy file | annotate | diff | comparison | revisions src/HOL/Set.thy file | annotate | diff | comparison | revisions
```--- 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"

+lemma member_bind [simp]:
+  "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
+
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 = {}"