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
```