author | nipkow |
Fri, 01 May 2015 08:45:30 +0200 | |
changeset 60161 | 59ebc3f2f896 |
parent 60160 | 52aa014308cb |
child 60165 | 29c826137153 |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Set.thy Thu Apr 30 16:07:43 2015 +0200 +++ b/src/HOL/Set.thy Fri May 01 08:45:30 2015 +0200 @@ -1623,6 +1623,9 @@ lemma Pow_empty [simp]: "Pow {} = {{}}" by (auto simp add: Pow_def) +lemma Pow_singleton_iff [simp]: "Pow X = {Y} \<longleftrightarrow> X = {} \<and> Y = {}" +by blast + lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)" by (blast intro: image_eqI [where ?x = "u - {a}" for u])