# HG changeset patch
# User paulson
# Date 1047634215 -3600
# Node ID b681a3cb0beb08bfdc2a24c6bd4daf55802e4d5b
# Parent  adf68d9e5dec8ba3b8c46d80182efe38d9b302a0
new UN/INT simprules

diff -r adf68d9e5dec -r b681a3cb0beb src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Mar 13 18:54:38 2003 +0100
+++ b/src/HOL/Set.thy	Fri Mar 14 10:30:15 2003 +0100
@@ -1657,7 +1657,8 @@
   by rules
 
 
-text {* \medskip Miniscoping: pushing in big Unions and Intersections. *}
+text {* \medskip Miniscoping: pushing in quantifiers and big Unions
+           and Intersections. *}
 
 lemma UN_simps [simp]:
   "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"
@@ -1722,6 +1723,35 @@
   by blast
 
 
+text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
+
+lemma UN_extend_simps:
+  "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))"
+  "!!A B C. (UN x:C. A x) Un B    = (if C={} then B else (UN x:C. A x Un B))"
+  "!!A B C. A Un (UN x:C. B x)   = (if C={} then A else (UN x:C. A Un B x))"
+  "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)"
+  "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)"
+  "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)"
+  "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)"
+  "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)"
+  "!!A B C. (UN  x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
+  "!!A B f. (UN a:A. B (f a)) = (UN x:f`A. B x)"
+  by auto
+
+lemma INT_extend_simps:
+  "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))"
+  "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))"
+  "!!A B C. (INT x:C. A x) - B   = (if C={} then UNIV-B else (INT x:C. A x - B))"
+  "!!A B C. A - (UN x:C. B x)   = (if C={} then A else (INT x:C. A - B x))"
+  "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))"
+  "!!A B C. ((INT x:C. A x) Un B)  = (INT x:C. A x Un B)"
+  "!!A B C. A Un (INT x:C. B x)  = (INT x:C. A Un B x)"
+  "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)"
+  "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)"
+  "!!A B f. (INT a:A. B (f a))    = (INT x:f`A. B x)"
+  by auto
+
+
 subsubsection {* Monotonicity of various operations *}
 
 lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"