diff -r 804dfa6d35b6 -r bdf8eb8f126b src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Sep 06 11:31:01 2011 +0200 +++ b/src/HOL/Set.thy Tue Sep 06 14:25:16 2011 +0200 @@ -785,6 +785,26 @@ lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)" by auto +lemma insert_eq_iff: assumes "a \ A" "b \ B" +shows "insert a A = insert b B \ + (if a=b then A=B else \C. A = insert b C \ b \ C \ B = insert a C \ a \ C)" + (is "?L \ ?R") +proof + assume ?L + show ?R + proof cases + assume "a=b" with assms `?L` show ?R by (simp add: insert_ident) + next + assume "a\b" + let ?C = "A - {b}" + have "A = insert b ?C \ b \ ?C \ B = insert a ?C \ a \ ?C" + using assms `?L` `a\b` by auto + thus ?R using `a\b` by auto + qed +next + assume ?R thus ?L by(auto split: if_splits) +qed + subsubsection {* Singletons, using insert *} lemma singletonI [intro!,no_atp]: "a : {a}"