src/HOL/Set.thy
 changeset 44744 bdf8eb8f126b parent 44490 e3e8d20a6ebc child 45121 5e495ccf6e56
equal inserted replaced
44743:804dfa6d35b6 44744:bdf8eb8f126b
`   782   show "x \<notin> A - {x}" by blast`
`   782   show "x \<notin> A - {x}" by blast`
`   783 qed`
`   783 qed`
`   784 `
`   784 `
`   785 lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"`
`   785 lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"`
`   786 by auto`
`   786 by auto`
`       `
`   787 `
`       `
`   788 lemma insert_eq_iff: assumes "a \<notin> A" "b \<notin> B"`
`       `
`   789 shows "insert a A = insert b B \<longleftrightarrow>`
`       `
`   790   (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)"`
`       `
`   791   (is "?L \<longleftrightarrow> ?R")`
`       `
`   792 proof`
`       `
`   793   assume ?L`
`       `
`   794   show ?R`
`       `
`   795   proof cases`
`       `
`   796     assume "a=b" with assms `?L` show ?R by (simp add: insert_ident)`
`       `
`   797   next`
`       `
`   798     assume "a\<noteq>b"`
`       `
`   799     let ?C = "A - {b}"`
`       `
`   800     have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"`
`       `
`   801       using assms `?L` `a\<noteq>b` by auto`
`       `
`   802     thus ?R using `a\<noteq>b` by auto`
`       `
`   803   qed`
`       `
`   804 next`
`       `
`   805   assume ?R thus ?L by(auto split: if_splits)`
`       `
`   806 qed`
`   787 `
`   807 `
`   788 subsubsection {* Singletons, using insert *}`
`   808 subsubsection {* Singletons, using insert *}`
`   789 `
`   809 `
`   790 lemma singletonI [intro!,no_atp]: "a : {a}"`
`   810 lemma singletonI [intro!,no_atp]: "a : {a}"`
`   791     -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}`
`   811     -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}`