src/HOL/Set.thy
changeset 44744 bdf8eb8f126b
parent 44490 e3e8d20a6ebc
child 45121 5e495ccf6e56
     1.1 --- a/src/HOL/Set.thy	Tue Sep 06 11:31:01 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Sep 06 14:25:16 2011 +0200
     1.3 @@ -785,6 +785,26 @@
     1.4  lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
     1.5  by auto
     1.6  
     1.7 +lemma insert_eq_iff: assumes "a \<notin> A" "b \<notin> B"
     1.8 +shows "insert a A = insert b B \<longleftrightarrow>
     1.9 +  (if a=b then A=B else \<exists>C. A = insert b C \<and> b \<notin> C \<and> B = insert a C \<and> a \<notin> C)"
    1.10 +  (is "?L \<longleftrightarrow> ?R")
    1.11 +proof
    1.12 +  assume ?L
    1.13 +  show ?R
    1.14 +  proof cases
    1.15 +    assume "a=b" with assms `?L` show ?R by (simp add: insert_ident)
    1.16 +  next
    1.17 +    assume "a\<noteq>b"
    1.18 +    let ?C = "A - {b}"
    1.19 +    have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"
    1.20 +      using assms `?L` `a\<noteq>b` by auto
    1.21 +    thus ?R using `a\<noteq>b` by auto
    1.22 +  qed
    1.23 +next
    1.24 +  assume ?R thus ?L by(auto split: if_splits)
    1.25 +qed
    1.26 +
    1.27  subsubsection {* Singletons, using insert *}
    1.28  
    1.29  lemma singletonI [intro!,no_atp]: "a : {a}"