src/HOL/Set.thy
 changeset 14302 6c24235e8d5d parent 14208 144f45277d5a child 14335 9c0b5e081037
```     1.1 --- a/src/HOL/Set.thy	Thu Dec 18 15:06:24 2003 +0100
1.2 +++ b/src/HOL/Set.thy	Fri Dec 19 04:28:45 2003 +0100
1.3 @@ -895,6 +895,9 @@
1.4    apply (erule insertI2)
1.5    done
1.6
1.7 +lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
1.8 +by blast
1.9 +
1.10  lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
1.11    by blast
1.12
1.13 @@ -961,6 +964,9 @@
1.14  lemma Diff_subset: "A - B \<subseteq> A"
1.15    by blast
1.16
1.17 +lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
1.18 +by blast
1.19 +
1.20
1.21  text {* \medskip Monotonicity. *}
1.22
1.23 @@ -1052,6 +1058,9 @@
1.24  lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
1.25    by blast
1.26
1.27 +lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
1.28 +by blast
1.29 +
1.30  lemma insert_disjoint[simp]:
1.31   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
1.32  by blast
1.33 @@ -1495,6 +1504,9 @@
1.34  lemma Diff_cancel [simp]: "A - A = {}"
1.35    by blast
1.36
1.37 +lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
1.38 +by blast
1.39 +
1.40  lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
1.41    by (blast elim: equalityE)
1.42
1.43 @@ -1524,6 +1536,9 @@
1.44  lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
1.45    by blast
1.46
1.47 +lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
1.48 +by blast
1.49 +
1.50  lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
1.51    by blast
1.52
```