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