Added a few thms about UN/INT/{}/UNIV
authornipkow
Fri Oct 18 09:53:02 2002 +0200 (2002-10-18)
changeset 13653ef123b9e8089
parent 13652 172600c40793
child 13654 b0d8bad27f42
Added a few thms about UN/INT/{}/UNIV
src/HOL/Set.ML
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.ML	Thu Oct 17 10:56:00 2002 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Oct 18 09:53:02 2002 +0200
     1.3 @@ -161,7 +161,6 @@
     1.4  val UN_constant = thm "UN_constant";
     1.5  val UN_empty = thm "UN_empty";
     1.6  val UN_empty2 = thm "UN_empty2";
     1.7 -val UN_empty3 = thm "UN_empty3";
     1.8  val UN_eq = thm "UN_eq";
     1.9  val UN_iff = thm "UN_iff";
    1.10  val UN_insert = thm "UN_insert";
     2.1 --- a/src/HOL/Set.thy	Thu Oct 17 10:56:00 2002 +0200
     2.2 +++ b/src/HOL/Set.thy	Fri Oct 18 09:53:02 2002 +0200
     2.3 @@ -1292,7 +1292,10 @@
     2.4    by blast
     2.5  
     2.6  lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
     2.7 -  by auto
     2.8 +  by blast
     2.9 +
    2.10 +lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
    2.11 +  by blast
    2.12  
    2.13  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
    2.14    by blast
    2.15 @@ -1315,6 +1318,11 @@
    2.16  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
    2.17    by blast
    2.18  
    2.19 +lemma Inter_UNIV_conv [iff]:
    2.20 +  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
    2.21 +  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
    2.22 +  by(blast)+
    2.23 +
    2.24  
    2.25  text {*
    2.26    \medskip @{text UN} and @{text INT}.
    2.27 @@ -1386,8 +1394,15 @@
    2.28    -- {* Look: it has an \emph{existential} quantifier *}
    2.29    by blast
    2.30  
    2.31 -lemma UN_empty3 [iff]: "(UNION A B = {}) = (\<forall>x\<in>A. B x = {})"
    2.32 -  by auto
    2.33 +lemma UNION_empty_conv[iff]:
    2.34 +  "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
    2.35 +  "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
    2.36 +by blast+
    2.37 +
    2.38 +lemma INTER_UNIV_conv[iff]:
    2.39 + "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
    2.40 + "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
    2.41 +by blast+
    2.42  
    2.43  
    2.44  text {* \medskip Distributive laws: *}