src/HOL/Set.thy
changeset 60057 86fa63ce8156
parent 59507 b468e0f8da2a
child 60161 59ebc3f2f896
     1.1 --- a/src/HOL/Set.thy	Mon Apr 13 13:03:41 2015 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Apr 14 11:32:01 2015 +0200
     1.3 @@ -647,7 +647,6 @@
     1.4  lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
     1.5  by blast
     1.6  
     1.7 -
     1.8  subsubsection {* The Powerset operator -- Pow *}
     1.9  
    1.10  definition Pow :: "'a set => 'a set set" where
    1.11 @@ -846,6 +845,9 @@
    1.12    assume ?R thus ?L by (auto split: if_splits)
    1.13  qed
    1.14  
    1.15 +lemma insert_UNIV: "insert x UNIV = UNIV"
    1.16 +by auto
    1.17 +
    1.18  subsubsection {* Singletons, using insert *}
    1.19  
    1.20  lemma singletonI [intro!]: "a : {a}"
    1.21 @@ -1884,6 +1886,8 @@
    1.22  lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
    1.23    by (auto simp add: bind_def)
    1.24  
    1.25 +lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
    1.26 +  by(auto simp add: bind_def)
    1.27  
    1.28  subsubsection {* Operations for execution *}
    1.29