# HG changeset patch
# User nipkow
# Date 1034927582 -7200
# Node ID ef123b9e80896ac9a11a3435febfacba5acf6e7b
# Parent  172600c4079305c590904fd99376b6e03cd7fb6b
Added a few thms about UN/INT/{}/UNIV

diff -r 172600c40793 -r ef123b9e8089 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Oct 17 10:56:00 2002 +0200
+++ b/src/HOL/Set.ML	Fri Oct 18 09:53:02 2002 +0200
@@ -161,7 +161,6 @@
 val UN_constant = thm "UN_constant";
 val UN_empty = thm "UN_empty";
 val UN_empty2 = thm "UN_empty2";
-val UN_empty3 = thm "UN_empty3";
 val UN_eq = thm "UN_eq";
 val UN_iff = thm "UN_iff";
 val UN_insert = thm "UN_insert";
diff -r 172600c40793 -r ef123b9e8089 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 17 10:56:00 2002 +0200
+++ b/src/HOL/Set.thy	Fri Oct 18 09:53:02 2002 +0200
@@ -1292,7 +1292,10 @@
   by blast
 
 lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
-  by auto
+  by blast
+
+lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
+  by blast
 
 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
   by blast
@@ -1315,6 +1318,11 @@
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by blast
 
+lemma Inter_UNIV_conv [iff]:
+  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
+  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
+  by(blast)+
+
 
 text {*
   \medskip @{text UN} and @{text INT}.
@@ -1386,8 +1394,15 @@
   -- {* Look: it has an \emph{existential} quantifier *}
   by blast
 
-lemma UN_empty3 [iff]: "(UNION A B = {}) = (\<forall>x\<in>A. B x = {})"
-  by auto
+lemma UNION_empty_conv[iff]:
+  "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
+  "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
+by blast+
+
+lemma INTER_UNIV_conv[iff]:
+ "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
+ "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
+by blast+
 
 
 text {* \medskip Distributive laws: *}