# HG changeset patch
# User lcp
# Date 783860296 -3600
# Node ID 0727f0c0c4f0bfc1c85a827edf131d8ac50d12a6
# Parent  527902f96cf2ed098442986d84d8d50a19247de2
ZF/equalities/domain_converse,range_converse,
prod_Un_distrib2,prod_Int_distrib2: new

diff -r 527902f96cf2 -r 0727f0c0c4f0 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Thu Nov 03 11:52:04 1994 +0100
+++ b/src/ZF/equalities.ML	Thu Nov 03 11:58:16 1994 +0100
@@ -282,6 +282,11 @@
 by (fast_tac eq_cs 1);
 val SUM_Un_distrib2 = result();
 
+(*First-order version of the above, for rewriting*)
+goal ZF.thy "I * (A Un B) = I*A Un I*B";
+by (resolve_tac [SUM_Un_distrib2] 1);
+val prod_Un_distrib2 = result();
+
 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();
@@ -291,6 +296,11 @@
 by (fast_tac eq_cs 1);
 val SUM_Int_distrib2 = result();
 
+(*First-order version of the above, for rewriting*)
+goal ZF.thy "I * (A Int B) = I*A Int I*B";
+by (resolve_tac [SUM_Int_distrib2] 1);
+val prod_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);
@@ -320,6 +330,12 @@
 by (fast_tac eq_cs 1);
 val domain_diff_subset = result();
 
+goal ZF.thy "domain(converse(r)) = range(r)";
+by (fast_tac eq_cs 1);
+val domain_converse = result();
+
+
+
 (** Range **)
 
 val range_of_prod = prove_goal ZF.thy
@@ -345,6 +361,10 @@
 by (fast_tac eq_cs 1);
 val range_diff_subset = result();
 
+goal ZF.thy "range(converse(r)) = domain(r)";
+by (fast_tac eq_cs 1);
+val range_converse = result();
+
 (** Field **)
 
 val field_of_prod = prove_goal ZF.thy "field(A*A) = A"