src/ZF/equalities.ML
changeset 1568 630d881b51bd
parent 1461 6bcb44e4d6e5
child 1611 35e0fd1b1775
equal deleted inserted replaced
1567:02bbdc811ae7 1568:630d881b51bd
   188 
   188 
   189 goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
   189 goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
   190 by (fast_tac (eq_cs addSEs [equalityE]) 1);
   190 by (fast_tac (eq_cs addSEs [equalityE]) 1);
   191 qed "Union_disjoint";
   191 qed "Union_disjoint";
   192 
   192 
       
   193 goal ZF.thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
       
   194 by (fast_tac ZF_cs 1);
       
   195 qed "Inter_Un_subset";
       
   196 
   193 (* A good challenge: Inter is ill-behaved on the empty set *)
   197 (* A good challenge: Inter is ill-behaved on the empty set *)
   194 goal ZF.thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
   198 goal ZF.thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
   195 by (fast_tac eq_cs 1);
   199 by (fast_tac eq_cs 1);
   196 qed "Inter_Un_distrib";
   200 qed "Inter_Un_distrib";
   197 
   201