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"