# 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)";