# HG changeset patch
# User paulson
# Date 1022252128 -7200
# Node ID bc54319f687594d14c413fd2648336ab026bdf9f
# Parent  ba734cc2887d998b12b40be40b66e11670878369
new quantifier lemmas

diff -r ba734cc2887d -r bc54319f6875 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Fri May 24 15:24:29 2002 +0200
+++ b/src/ZF/equalities.thy	Fri May 24 16:55:28 2002 +0200
@@ -26,6 +26,23 @@
 lemma the_eq_0 [simp]: "(THE x. False) = 0"
 by (blast intro: the_0)
 
+text {* \medskip Bounded quantifiers.
+
+  The following are not added to the default simpset because
+  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
+
+lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
+  by blast
+
+lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
+  by blast
+
+lemma ball_UN: "(\<forall>z \<in> (UN x:A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
+  by blast
+
+lemma bex_UN: "(\<exists>z \<in> (UN x:A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
+  by blast
+
 (*** converse ***)
 
 lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>:r"