# HG changeset patch
# User haftmann
# Date 1190831278 -7200
# Node ID a87d8d31abc0b6ab385c80c714a5ddb044305b13
# Parent  f5015dd2431b7a3b3238c012490318ac92dfceaf
convenient obtain rule for sets

diff -r f5015dd2431b -r a87d8d31abc0 src/HOL/Set.thy
--- 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 *}