author | haftmann |
Wed, 26 Sep 2007 20:27:58 +0200 | |
changeset 24730 | a87d8d31abc0 |
parent 24729 | f5015dd2431b |
child 24731 | c25aa6ae64ec |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Set.thy Wed Sep 26 20:27:57 2007 +0200 +++ b/src/HOL/Set.thy Wed Sep 26 20:27:58 2007 +0200 @@ -771,6 +771,15 @@ lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)" by auto +lemma set_insert: + assumes "x \<in> A" + obtains B where "A = insert x B" and "x \<notin> B" +proof + from assms show "A = insert x (A - {x})" by blast +next + show "x \<notin> A - {x}" by blast +qed + subsubsection {* Singletons, using insert *}