more lemmas
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Fri Oct 07 17:59:19 2016 +0200 (2016-10-07)
changeset 640776d770c2dc60d
parent 64076 9f089287687b
child 64093 f09f377da49d
more lemmas
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 07 17:58:36 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 07 17:59:19 2016 +0200
     1.3 @@ -656,6 +656,9 @@
     1.4  lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
     1.5    by (auto simp: subset_mset_def elim: mset_add)
     1.6  
     1.7 +lemma Diff_eq_empty_iff_mset: "A - B = {#} \<longleftrightarrow> A \<subseteq># B"
     1.8 +  by (auto simp: multiset_eq_iff subseteq_mset_def)
     1.9 +
    1.10  
    1.11  subsubsection \<open>Intersection and bounded union\<close>
    1.12  
    1.13 @@ -749,6 +752,12 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 +lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}"
    1.18 +  by (meson disjunct_not_in union_iff)
    1.19 +
    1.20 +lemma inter_mset_empty_distrib_left: "(A + B) \<inter># C = {#} \<longleftrightarrow> A \<inter># C = {#} \<and> B \<inter># C = {#}"
    1.21 +  by (meson disjunct_not_in union_iff)
    1.22 +
    1.23  lemma add_mset_inter_add_mset[simp]:
    1.24    "add_mset a A \<inter># add_mset a B = add_mset a (A \<inter># B)"
    1.25    by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
    1.26 @@ -1305,6 +1314,9 @@
    1.27    qed
    1.28  qed
    1.29  
    1.30 +lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \<in># M. Q x \<and> P x#}"
    1.31 +  by (auto simp: multiset_eq_iff)
    1.32 +
    1.33  
    1.34  subsubsection \<open>Size\<close>
    1.35  
    1.36 @@ -1732,6 +1744,12 @@
    1.37  lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
    1.38  by (induct x) auto
    1.39  
    1.40 +lemma mset_single_iff[iff]: "mset xs = {#x#} \<longleftrightarrow> xs = [x]"
    1.41 +  by (cases xs) auto
    1.42 +
    1.43 +lemma mset_single_iff_right[iff]: "{#x#} = mset xs \<longleftrightarrow> xs = [x]"
    1.44 +  by (cases xs) auto
    1.45 +
    1.46  lemma set_mset_mset[simp]: "set_mset (mset xs) = set xs"
    1.47    by (induct xs) auto
    1.48  
    1.49 @@ -2033,6 +2051,9 @@
    1.50  lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> A = {#}"
    1.51    by (auto simp: multiset_eq_iff)
    1.52  
    1.53 +lemma repeat_mset_eq_empty_iff: "repeat_mset n A = {#} \<longleftrightarrow> n = 0 \<or> A = {#}"
    1.54 +  by (cases n) auto
    1.55 +
    1.56  lemma image_replicate_mset [simp]:
    1.57    "image_mset f (replicate_mset n a) = replicate_mset n (f a)"
    1.58    by (induct n) simp_all