# HG changeset patch
# User paulson
# Date 828634728 -7200
# Node ID 9b78ce58d6b16f2e94e29db5e613067d851ccd09
# Parent  ab0da8a9ae3ec89707bb53787791e185b9ece555
Proved Inter_0 and converse_INT

diff -r ab0da8a9ae3e -r 9b78ce58d6b1 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Thu Apr 04 18:18:08 1996 +0200
+++ b/src/ZF/equalities.ML	Thu Apr 04 18:18:48 1996 +0200
@@ -194,6 +194,10 @@
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
+goalw ZF.thy [Inter_def] "Inter(0) = 0";
+by (fast_tac eq_cs 1);
+qed "Inter_0";
+
 goal ZF.thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
 by (fast_tac ZF_cs 1);
 qed "Inter_Un_subset";
@@ -480,11 +484,15 @@
 by (fast_tac eq_cs 1);
 qed "converse_Diff";
 
-(*Does the analogue hold for INT?*)
 goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
 by (fast_tac eq_cs 1);
 qed "converse_UN";
 
+(*Unfolding Inter avoids using excluded middle on A=0*)
+goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
+by (fast_tac eq_cs 1);
+qed "converse_INT";
+
 (** Pow **)
 
 goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";