src/HOL/Set.thy

--- a/src/HOL/Set.thy	Thu Dec 18 15:06:24 2003 +0100
+++ b/src/HOL/Set.thy	Fri Dec 19 04:28:45 2003 +0100
@@ -895,6 +895,9 @@
   apply (erule insertI2)
   done
 
+lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
+by blast
+
 lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
   by blast
 
@@ -961,6 +964,9 @@
 lemma Diff_subset: "A - B \<subseteq> A"
   by blast
 
+lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
+by blast
+
 
 text {* \medskip Monotonicity. *}
 
@@ -1052,6 +1058,9 @@
 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   by blast
 
+lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
+by blast
+
 lemma insert_disjoint[simp]:
  "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
 by blast
@@ -1495,6 +1504,9 @@
 lemma Diff_cancel [simp]: "A - A = {}"
   by blast
 
+lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
+by blast
+
 lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
   by (blast elim: equalityE)
 
@@ -1524,6 +1536,9 @@
 lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
   by blast
 
+lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
+by blast
+
 lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
   by blast