src/HOL/Library/DAList_Multiset.thy
changeset 64587 8355a6e2df79
parent 63830 2ea3725a34bd
child 66148 5e60c2d0a1f1
     1.1 --- a/src/HOL/Library/DAList_Multiset.thy	Sat Dec 17 15:22:00 2016 +0100
     1.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -228,17 +228,17 @@
     1.4    by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
     1.5  
     1.6  
     1.7 -lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
     1.8 +lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<subseteq># m2 \<and> m2 \<subseteq># m1"
     1.9    by (metis equal_multiset_def subset_mset.eq_iff)
    1.10  
    1.11  text \<open>By default the code for \<open><\<close> is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
    1.12  With equality implemented by \<open>\<le>\<close>, this leads to three calls of  \<open>\<le>\<close>.
    1.13  Here is a more efficient version:\<close>
    1.14 -lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
    1.15 +lemma mset_less[code]: "xs \<subset># (ys :: 'a multiset) \<longleftrightarrow> xs \<subseteq># ys \<and> \<not> ys \<subseteq># xs"
    1.16    by (rule subset_mset.less_le_not_le)
    1.17  
    1.18  lemma mset_less_eq_Bag0:
    1.19 -  "Bag xs \<le># A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
    1.20 +  "Bag xs \<subseteq># A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
    1.21      (is "?lhs \<longleftrightarrow> ?rhs")
    1.22  proof
    1.23    assume ?lhs
    1.24 @@ -255,7 +255,7 @@
    1.25  qed
    1.26  
    1.27  lemma mset_less_eq_Bag [code]:
    1.28 -  "Bag xs \<le># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
    1.29 +  "Bag xs \<subseteq># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
    1.30  proof -
    1.31    {
    1.32      fix x n