src/HOL/Set.thy
changeset 32456 341c83339aeb
parent 32264 0be31453f698
child 32683 7c1fe854ca6a
     1.1 --- a/src/HOL/Set.thy	Sat Aug 29 14:31:39 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Aug 31 14:09:42 2009 +0200
     1.3 @@ -1268,10 +1268,26 @@
     1.4      "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
     1.5    by auto
     1.6  
     1.7 +lemma Int_insert_left_if0[simp]:
     1.8 +    "a \<notin> C \<Longrightarrow> (insert a B) Int C = B \<inter> C"
     1.9 +  by auto
    1.10 +
    1.11 +lemma Int_insert_left_if1[simp]:
    1.12 +    "a \<in> C \<Longrightarrow> (insert a B) Int C = insert a (B Int C)"
    1.13 +  by auto
    1.14 +
    1.15  lemma Int_insert_right:
    1.16      "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
    1.17    by auto
    1.18  
    1.19 +lemma Int_insert_right_if0[simp]:
    1.20 +    "a \<notin> A \<Longrightarrow> A Int (insert a B) = A Int B"
    1.21 +  by auto
    1.22 +
    1.23 +lemma Int_insert_right_if1[simp]:
    1.24 +    "a \<in> A \<Longrightarrow> A Int (insert a B) = insert a (A Int B)"
    1.25 +  by auto
    1.26 +
    1.27  lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
    1.28    by blast
    1.29