src/HOL/Set.thy
changeset 14742 dde816115d6a
parent 14692 b8d6c395c9e2
child 14752 3fc3c7b7e99d
     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}. *}