--- a/src/HOL/Set.thy Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Set.thy Tue Apr 14 11:32:01 2015 +0200
@@ -647,7 +647,6 @@
lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
by blast
-
subsubsection {* The Powerset operator -- Pow *}
definition Pow :: "'a set => 'a set set" where
@@ -846,6 +845,9 @@
assume ?R thus ?L by (auto split: if_splits)
qed
+lemma insert_UNIV: "insert x UNIV = UNIV"
+by auto
+
subsubsection {* Singletons, using insert *}
lemma singletonI [intro!]: "a : {a}"
@@ -1884,6 +1886,8 @@
lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
by (auto simp add: bind_def)
+lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
+ by(auto simp add: bind_def)
subsubsection {* Operations for execution *}