author paulson Tue, 24 Sep 1996 13:53:18 +0200 changeset 2021 dd5866263153 parent 2020 586f3c075b05 child 2022 9d47e2962edd
Added miniscoping for UN and INT
 src/HOL/equalities.ML file | annotate | diff | comparison | revisions
```--- 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";

+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";

+
+
+(** 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