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: *}