author paulson Mon, 17 Mar 2003 17:37:20 +0100 changeset 13865 0a6bf71955b0 parent 13864 f44f121dd275 child 13866 b42d7983a822
 src/HOL/Set.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Set.thy	Fri Mar 14 18:00:16 2003 +0100
+++ b/src/HOL/Set.thy	Mon Mar 17 17:37:20 2003 +0100
@@ -229,12 +229,6 @@
lemma CollectD: "a : {x. P(x)} ==> P(a)"
by simp

-lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
-  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
-   apply (rule Collect_mem_eq)
-  apply (rule Collect_mem_eq)
-  done
-
lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
by simp

@@ -408,6 +402,12 @@

subsubsection {* Equality *}

+lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
+  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
+   apply (rule Collect_mem_eq)
+  apply (rule Collect_mem_eq)
+  done
+
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
-- {* Anti-symmetry of the subset relation. *}
by (rules intro: set_ext subsetD)
@@ -451,6 +451,9 @@
lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
by simp

+lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"
+  by simp
+

subsubsection {* The universal set -- UNIV *}
```