# HG changeset patch
# User mehta
# Date 1084456949 -7200
# Node ID dde816115d6ae8476a21294e25768a50c0ccc074
# Parent  36582c356db7a00e2cd714e81ccc84ce95456bd0
New simp rules added:

insert_disjoint
disjoint_insert
disjoint_int_union

diff -r 36582c356db7 -r dde816115d6a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed May 12 10:40:41 2004 +0200
+++ b/src/HOL/Set.thy	Thu May 13 16:02:29 2004 +0200
@@ -1095,14 +1095,20 @@
   by blast
 
 lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
-by blast
+  by blast
 
 lemma insert_disjoint[simp]:
  "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
-by blast
+ "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
+by auto
 
 lemma disjoint_insert[simp]:
  "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
+ "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
+by auto
+
+lemma disjoint_int_union[simp]:
+  "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B \<and> {} = A \<inter> C)"
 by blast
 
 text {* \medskip @{text image}. *}