# HG changeset patch
# User paulson
# Date 864732255 -7200
# Node ID 9b899eb8a0361d11195230cce4183d28d8d12b31
# Parent  0d955bcf8e0a4ef619f2bb40c6d65772fa141375
New theorem disjoint_eq_subset_Compl

diff -r 0d955bcf8e0a -r 9b899eb8a036 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue May 27 13:23:53 1997 +0200
+++ b/src/HOL/equalities.ML	Tue May 27 13:24:15 1997 +0200
@@ -151,6 +151,10 @@
 qed "Int_empty_right";
 Addsimps[Int_empty_right];
 
+goal Set.thy "(A Int B = {}) = (A <= Compl B)";
+by (blast_tac (!claset addSEs [equalityE]) 1);
+qed "disjoint_eq_subset_Compl";
+
 goal Set.thy "UNIV Int B = B";
 by (Blast_tac 1);
 qed "Int_UNIV_left";
@@ -229,6 +233,18 @@
 by (Blast_tac 1);
 qed "Un_insert_right";
 
+goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
+\                                          else        B Int C)";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (Blast_tac 1);
+qed "Int_insert_left";
+
+goal Set.thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
+\                                          else        A Int B)";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (Blast_tac 1);
+qed "Int_insert_right";
+
 goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
 by (Blast_tac 1);
 qed "Un_Int_distrib";