src/HOL/Set.thy
 changeset 13653 ef123b9e8089 parent 13624 17684cf64fda child 13763 f94b569cd610
     1.1 --- a/src/HOL/Set.thy	Thu Oct 17 10:56:00 2002 +0200
1.2 +++ b/src/HOL/Set.thy	Fri Oct 18 09:53:02 2002 +0200
1.3 @@ -1292,7 +1292,10 @@
1.4    by blast
1.5
1.6  lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
1.7 -  by auto
1.8 +  by blast
1.9 +
1.10 +lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
1.11 +  by blast
1.12
1.13  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
1.14    by blast
1.15 @@ -1315,6 +1318,11 @@
1.16  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
1.17    by blast
1.18
1.19 +lemma Inter_UNIV_conv [iff]:
1.20 +  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
1.21 +  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
1.22 +  by(blast)+
1.23 +
1.24
1.25  text {*
1.26    \medskip @{text UN} and @{text INT}.
1.27 @@ -1386,8 +1394,15 @@
1.28    -- {* Look: it has an \emph{existential} quantifier *}
1.29    by blast
1.30
1.31 -lemma UN_empty3 [iff]: "(UNION A B = {}) = (\<forall>x\<in>A. B x = {})"
1.32 -  by auto
1.33 +lemma UNION_empty_conv[iff]:
1.34 +  "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
1.35 +  "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
1.36 +by blast+
1.37 +
1.38 +lemma INTER_UNIV_conv[iff]:
1.39 + "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
1.40 + "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
1.41 +by blast+
1.42
1.43
1.44  text {* \medskip Distributive laws: *}