# HG changeset patch
# User paulson
# Date 843565998 -7200
# Node ID dd5866263153951a8b5502f4c5fb77702296fd78
# Parent  586f3c075b05d8cc173531e114799c133d803bd4
Added miniscoping for UN and INT

diff -r 586f3c075b05 -r dd5866263153 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Sep 24 13:51:10 1996 +0200
+++ b/src/HOL/equalities.ML	Tue Sep 24 13:53:18 1996 +0200
@@ -366,6 +366,15 @@
 qed "INT_insert";
 Addsimps[INT_insert];
 
+goal Set.thy
+    "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
+by (Fast_tac 1);
+qed "INT_insert_distrib";
+
+goal Set.thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
+by (Fast_tac 1);
+qed "INT1_insert_distrib";
+
 goal Set.thy "Union(range(f)) = (UN x.f(x))";
 by (Fast_tac 1);
 qed "Union_range_eq";
@@ -531,3 +540,33 @@
 qed "Diff_Int";
 
 Addsimps[subset_UNIV, empty_subsetI, subset_refl];
+
+
+(** Miniscoping: pushing in big Unions and Intersections **)
+local
+  fun prover s = prove_goal Set.thy s (fn _ => [Fast_tac 1])
+in
+val UN1_simps = map prover 
+		["(UN x. insert a (B x)) = insert a (UN x. B x)",
+		 "(UN x. A x Int B)  = ((UN x.A x) Int B)",
+		 "(UN x. A Int B x)  = (A Int (UN x.B x))",
+		 "(UN x. A x Un B)   = ((UN x.A x) Un B)",
+		 "(UN x. A Un B x)   = (A Un (UN x.B x))",
+		 "(UN x. A x - B)    = ((UN x.A x) - B)",
+		 "(UN x. A - B x)    = (A - (INT x.B x))"];
+
+val INT1_simps = map prover
+		["(INT x. insert a (B x)) = insert a (INT x. B x)",
+		 "(INT x. A x Int B) = ((INT x.A x) Int B)",
+		 "(INT x. A Int B x) = (A Int (INT x.B x))",
+		 "(INT x. A x Un B)  = ((INT x.A x) Un B)",
+		 "(INT x. A Un B x)  = (A Un (INT x.B x))",
+		 "(INT x. A x - B)   = ((INT x.A x) - B)",
+		 "(INT x. A - B x)   = (A - (UN x.B x))"];
+
+(*Analogous laws for bounded Unions and Intersections are conditional
+  on the index set's being non-empty.  Thus they are probably NOT worth 
+  adding as default rewrites.*)
+end;
+
+Addsimps (UN1_simps @ INT1_simps);