author paulson Mon Mar 17 17:37:20 2003 +0100 (2003-03-17) changeset 13865 0a6bf71955b0 parent 13864 f44f121dd275 child 13866 b42d7983a822
 src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Set.thy	Fri Mar 14 18:00:16 2003 +0100
1.2 +++ b/src/HOL/Set.thy	Mon Mar 17 17:37:20 2003 +0100
1.3 @@ -229,12 +229,6 @@
1.4  lemma CollectD: "a : {x. P(x)} ==> P(a)"
1.5    by simp
1.6
1.7 -lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
1.8 -  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
1.9 -   apply (rule Collect_mem_eq)
1.10 -  apply (rule Collect_mem_eq)
1.11 -  done
1.12 -
1.13  lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
1.14    by simp
1.15
1.16 @@ -408,6 +402,12 @@
1.17
1.18  subsubsection {* Equality *}
1.19
1.20 +lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
1.21 +  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
1.22 +   apply (rule Collect_mem_eq)
1.23 +  apply (rule Collect_mem_eq)
1.24 +  done
1.25 +
1.26  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
1.27    -- {* Anti-symmetry of the subset relation. *}
1.28    by (rules intro: set_ext subsetD)
1.29 @@ -451,6 +451,9 @@
1.30  lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
1.31    by simp
1.32
1.33 +lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)"
1.34 +  by simp
1.35 +
1.36
1.37  subsubsection {* The universal set -- UNIV *}
1.38
```