# HG changeset patch
# User lcp
# Date 755516352 -3600
# Node ID 3dc5c8016a0eb9e73dd2fb3522c6034e9168fd9c
# Parent  fe5d88d4c7e1da937e724a26efcf9dd71800d8c9
ZF/equalities/SUM_eq_UN: new
ZF/equalities: corrected bound variable anomalies in some distributive laws

diff -r fe5d88d4c7e1 -r 3dc5c8016a0e src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Fri Dec 10 10:36:39 1993 +0100
+++ b/src/ZF/equalities.ML	Fri Dec 10 10:39:12 1993 +0100
@@ -217,13 +217,13 @@
 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
     Union of a family of unions **)
 
-goal ZF.thy "(UN i:I. A(x) Un B(x)) = (UN i:I. A(x))  Un  (UN i:I. B(x))";
+goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
 by (fast_tac eq_cs 1);
 val UN_Un_distrib = result();
 
 goal ZF.thy
     "!!A B. i:I ==> \
-\           (INT i:I. A(x)  Int  B(x)) = (INT i:I. A(x)) Int (INT i:I. B(x))";
+\           (INT i:I. A(i)  Int  B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
 by (fast_tac eq_cs 1);
 val INT_Int_distrib = result();
 
@@ -243,28 +243,32 @@
 by (fast_tac eq_cs 1);
 val SUM_UN_distrib1 = result();
 
-goal ZF.thy "(SUM x:A. UN y:B. C(x,y)) = (UN y:B. SUM x:A. C(x,y))";
+goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
 by (fast_tac eq_cs 1);
 val SUM_UN_distrib2 = result();
 
-goal ZF.thy "(SUM x:A Un B. C(x)) = (SUM x:A. C(x)) Un (SUM x:B. C(x))";
+goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
 by (fast_tac eq_cs 1);
 val SUM_Un_distrib1 = result();
 
-goal ZF.thy
-    "(SUM i:I. A(x) Un B(x)) = (SUM i:I. A(x)) Un (SUM i:I. B(x))";
+goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
 by (fast_tac eq_cs 1);
 val SUM_Un_distrib2 = result();
 
-goal ZF.thy "(SUM x:A Int B. C(x)) = (SUM x:A. C(x)) Int (SUM x:B. C(x))";
+goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
 by (fast_tac eq_cs 1);
 val SUM_Int_distrib1 = result();
 
 goal ZF.thy
-    "(SUM i:I. A(x) Int B(x)) = (SUM i:I. A(x)) Int (SUM i:I. B(x))";
+    "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
 by (fast_tac eq_cs 1);
 val SUM_Int_distrib2 = result();
 
+(*Cf Aczel, Non-Well-Founded Sets, page 115*)
+goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
+by (fast_tac eq_cs 1);
+val SUM_eq_UN = result();
+
 (** Domain, Range and Field **)
 
 goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";