New simp rules added:
authormehta
Thu May 13 16:02:29 2004 +0200 (2004-05-13)
changeset 14742dde816115d6a
parent 14741 36582c356db7
child 14743 81001d6cb8c0
New simp rules added:

insert_disjoint
disjoint_insert
disjoint_int_union
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Wed May 12 10:40:41 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu May 13 16:02:29 2004 +0200
     1.3 @@ -1095,14 +1095,20 @@
     1.4    by blast
     1.5  
     1.6  lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
     1.7 -by blast
     1.8 +  by blast
     1.9  
    1.10  lemma insert_disjoint[simp]:
    1.11   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
    1.12 -by blast
    1.13 + "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
    1.14 +by auto
    1.15  
    1.16  lemma disjoint_insert[simp]:
    1.17   "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
    1.18 + "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
    1.19 +by auto
    1.20 +
    1.21 +lemma disjoint_int_union[simp]:
    1.22 +  "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B \<and> {} = A \<inter> C)"
    1.23  by blast
    1.24  
    1.25  text {* \medskip @{text image}. *}