normalising multiset theorem names
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Fri Jun 17 12:37:43 2016 +0200 (2016-06-17)
changeset 63310caaacf37943f
parent 63309 a77adb28a27a
child 63311 540cfb14a751
child 63320 b5bbf61b792f
normalising multiset theorem names
NEWS
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/Library/Permutation.thy
     1.1 --- a/NEWS	Thu Jun 16 17:11:00 2016 +0200
     1.2 +++ b/NEWS	Fri Jun 17 12:37:43 2016 +0200
     1.3 @@ -253,6 +253,37 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* The names of multiset theorems have been normalised to distinguish which
     1.8 +  ordering the theorems are about
     1.9 +    mset_less_eqI ~> mset_subset_eqI
    1.10 +    mset_less_insertD ~> mset_subset_insertD
    1.11 +    mset_less_eq_count ~> mset_subset_eq_count
    1.12 +    mset_less_diff_self ~> mset_subset_diff_self
    1.13 +    mset_le_exists_conv ~> mset_subset_eq_exists_conv
    1.14 +    mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel
    1.15 +    mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel
    1.16 +    mset_le_mono_add ~> mset_subset_eq_mono_add
    1.17 +    mset_le_add_left ~> mset_subset_eq_add_left
    1.18 +    mset_le_add_right ~> mset_subset_eq_add_right
    1.19 +    mset_le_single ~> mset_subset_eq_single
    1.20 +    mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute
    1.21 +    diff_le_self ~> diff_subset_eq_self
    1.22 +    mset_leD ~> mset_subset_eqD
    1.23 +    mset_lessD ~> mset_subsetD
    1.24 +    mset_le_insertD ~> mset_subset_eq_insertD
    1.25 +    mset_less_of_empty ~> mset_subset_of_empty
    1.26 +    le_empty ~> subset_eq_empty
    1.27 +    mset_less_add_bothsides ~> mset_subset_add_bothsides
    1.28 +    mset_less_empty_nonempty ~> mset_subset_empty_nonempty
    1.29 +    mset_less_size ~> mset_subset_size
    1.30 +    wf_less_mset_rel ~> wf_subset_mset_rel
    1.31 +    count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
    1.32 +    mset_remdups_le ~> mset_remdups_subset_eq
    1.33 +    ms_lesseq_impl ~> subset_eq_mset_impl
    1.34 +
    1.35 +  Some functions have been renamed:
    1.36 +    ms_lesseq_impl -> subset_eq_mset_impl
    1.37 +
    1.38  * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
    1.39  INCOMPATIBILITY.
    1.40  
     2.1 --- a/src/HOL/Library/DAList_Multiset.thy	Thu Jun 16 17:11:00 2016 +0200
     2.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Fri Jun 17 12:37:43 2016 +0200
     2.3 @@ -244,7 +244,7 @@
     2.4  next
     2.5    assume ?rhs
     2.6    show ?lhs
     2.7 -  proof (rule mset_less_eqI)
     2.8 +  proof (rule mset_subset_eqI)
     2.9      fix x
    2.10      from \<open>?rhs\<close> have "count_of (DAList.impl_of xs) x \<le> count A x"
    2.11        by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
     3.1 --- a/src/HOL/Library/Multiset.thy	Thu Jun 16 17:11:00 2016 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jun 17 12:37:43 2016 +0200
     3.3 @@ -456,15 +456,15 @@
     3.4    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
     3.5    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
     3.6  
     3.7 -lemma mset_less_eqI:
     3.8 +lemma mset_subset_eqI:
     3.9    "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
    3.10    by (simp add: subseteq_mset_def)
    3.11  
    3.12 -lemma mset_less_eq_count:
    3.13 +lemma mset_subset_eq_count:
    3.14    "A \<subseteq># B \<Longrightarrow> count A a \<le> count B a"
    3.15    by (simp add: subseteq_mset_def)
    3.16  
    3.17 -lemma mset_le_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
    3.18 +lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
    3.19    unfolding subseteq_mset_def
    3.20    apply (rule iffI)
    3.21     apply (rule exI [where x = "B - A"])
    3.22 @@ -472,31 +472,28 @@
    3.23    done
    3.24  
    3.25  interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" 0 "op \<le>#" "op <#" "op -"
    3.26 -  by standard (simp, fact mset_le_exists_conv)
    3.27 -
    3.28 -declare subset_mset.zero_order[simp del]
    3.29 -  \<comment> \<open>this removes some simp rules not in the usual order for multisets\<close>
    3.30 -
    3.31 -lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
    3.32 +  by standard (simp, fact mset_subset_eq_exists_conv)
    3.33 +
    3.34 +lemma mset_subset_eq_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
    3.35     by (fact subset_mset.add_le_cancel_right)
    3.36   
    3.37 -lemma mset_le_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
    3.38 +lemma mset_subset_eq_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
    3.39     by (fact subset_mset.add_le_cancel_left)
    3.40   
    3.41 -lemma mset_le_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
    3.42 +lemma mset_subset_eq_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
    3.43     by (fact subset_mset.add_mono)
    3.44   
    3.45 -lemma mset_le_add_left [simp]: "(A::'a multiset) \<subseteq># A + B"
    3.46 +lemma mset_subset_eq_add_left [simp]: "(A::'a multiset) \<subseteq># A + B"
    3.47     unfolding subseteq_mset_def by auto
    3.48   
    3.49 -lemma mset_le_add_right [simp]: "B \<subseteq># (A::'a multiset) + B"
    3.50 +lemma mset_subset_eq_add_right [simp]: "B \<subseteq># (A::'a multiset) + B"
    3.51     unfolding subseteq_mset_def by auto
    3.52   
    3.53  lemma single_subset_iff [simp]:
    3.54    "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
    3.55    by (auto simp add: subseteq_mset_def Suc_le_eq)
    3.56  
    3.57 -lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
    3.58 +lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
    3.59    by (simp add: subseteq_mset_def Suc_le_eq)
    3.60   
    3.61  lemma multiset_diff_union_assoc:
    3.62 @@ -504,16 +501,16 @@
    3.63    shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)"
    3.64    by (fact subset_mset.diff_add_assoc)
    3.65   
    3.66 -lemma mset_le_multiset_union_diff_commute:
    3.67 +lemma mset_subset_eq_multiset_union_diff_commute:
    3.68    fixes A B C D :: "'a multiset"
    3.69    shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B"
    3.70    by (fact subset_mset.add_diff_assoc2)
    3.71  
    3.72 -lemma diff_le_self[simp]:
    3.73 +lemma diff_subset_eq_self[simp]:
    3.74    "(M::'a multiset) - N \<subseteq># M"
    3.75    by (simp add: subseteq_mset_def)
    3.76  
    3.77 -lemma mset_leD:
    3.78 +lemma mset_subset_eqD:
    3.79    assumes "A \<subseteq># B" and "x \<in># A"
    3.80    shows "x \<in># B"
    3.81  proof -
    3.82 @@ -523,33 +520,33 @@
    3.83    finally show ?thesis by simp
    3.84  qed
    3.85    
    3.86 -lemma mset_lessD:
    3.87 +lemma mset_subsetD:
    3.88    "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
    3.89 -  by (auto intro: mset_leD [of A])
    3.90 +  by (auto intro: mset_subset_eqD [of A])
    3.91  
    3.92  lemma set_mset_mono:
    3.93    "A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
    3.94 -  by (metis mset_leD subsetI)
    3.95 -
    3.96 -lemma mset_le_insertD:
    3.97 +  by (metis mset_subset_eqD subsetI)
    3.98 +
    3.99 +lemma mset_subset_eq_insertD:
   3.100    "A + {#x#} \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   3.101  apply (rule conjI)
   3.102 - apply (simp add: mset_leD)
   3.103 + apply (simp add: mset_subset_eqD)
   3.104   apply (clarsimp simp: subset_mset_def subseteq_mset_def)
   3.105   apply safe
   3.106    apply (erule_tac x = a in allE)
   3.107    apply (auto split: if_split_asm)
   3.108  done
   3.109  
   3.110 -lemma mset_less_insertD:
   3.111 +lemma mset_subset_insertD:
   3.112    "A + {#x#} \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   3.113 -  by (rule mset_le_insertD) simp
   3.114 -
   3.115 -lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
   3.116 +  by (rule mset_subset_eq_insertD) simp
   3.117 +
   3.118 +lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
   3.119    by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff)
   3.120  
   3.121  lemma empty_le [simp]: "{#} \<subseteq># A"
   3.122 -  unfolding mset_le_exists_conv by auto
   3.123 +  unfolding mset_subset_eq_exists_conv by auto
   3.124   
   3.125  lemma insert_subset_eq_iff:
   3.126    "{#a#} + A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
   3.127 @@ -567,8 +564,8 @@
   3.128    "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
   3.129    by (simp add: subseteq_mset_def le_diff_conv)
   3.130  
   3.131 -lemma le_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
   3.132 -  unfolding mset_le_exists_conv by auto
   3.133 +lemma subset_eq_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
   3.134 +  unfolding mset_subset_eq_exists_conv by auto
   3.135  
   3.136  lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
   3.137    by (auto simp: subset_mset_def subseteq_mset_def)
   3.138 @@ -576,13 +573,13 @@
   3.139  lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False"
   3.140    by simp
   3.141  
   3.142 -lemma mset_less_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M"
   3.143 +lemma mset_subset_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M"
   3.144    by (fact subset_mset.add_less_imp_less_right)
   3.145  
   3.146 -lemma mset_less_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
   3.147 +lemma mset_subset_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
   3.148    by (fact subset_mset.zero_less_iff_neq_zero)
   3.149  
   3.150 -lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
   3.151 +lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
   3.152    by (auto simp: subset_mset_def elim: mset_add)
   3.153  
   3.154  
   3.155 @@ -822,13 +819,13 @@
   3.156    by (rule multiset_eqI) simp
   3.157  
   3.158  lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
   3.159 -  by (simp add: mset_less_eqI)
   3.160 +  by (simp add: mset_subset_eqI)
   3.161  
   3.162  lemma multiset_filter_mono:
   3.163    assumes "A \<subseteq># B"
   3.164    shows "filter_mset f A \<subseteq># filter_mset f B"
   3.165  proof -
   3.166 -  from assms[unfolded mset_le_exists_conv]
   3.167 +  from assms[unfolded mset_subset_eq_exists_conv]
   3.168    obtain C where B: "B = A + C" by auto
   3.169    show ?thesis unfolding B by auto
   3.170  qed
   3.171 @@ -840,7 +837,7 @@
   3.172  next
   3.173    assume ?Q
   3.174    then obtain Q where M: "M = N + Q"
   3.175 -    by (auto simp add: mset_le_exists_conv)
   3.176 +    by (auto simp add: mset_subset_eq_exists_conv)
   3.177    then have MN: "M - N = Q" by simp
   3.178    show ?P
   3.179    proof (rule multiset_eqI)
   3.180 @@ -943,7 +940,7 @@
   3.181    assumes "A \<subseteq># B"
   3.182    shows "size A \<le> size B"
   3.183  proof -
   3.184 -  from assms[unfolded mset_le_exists_conv]
   3.185 +  from assms[unfolded mset_subset_eq_exists_conv]
   3.186    obtain C where B: "B = A + C" by auto
   3.187    show ?thesis unfolding B by (induct C) auto
   3.188  qed
   3.189 @@ -953,7 +950,7 @@
   3.190  
   3.191  lemma size_Diff_submset:
   3.192    "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
   3.193 -by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
   3.194 +by (metis add_diff_cancel_left' size_union mset_subset_eq_exists_conv)
   3.195  
   3.196  
   3.197  subsection \<open>Induction and case splits\<close>
   3.198 @@ -988,10 +985,10 @@
   3.199  apply auto
   3.200  done
   3.201  
   3.202 -lemma mset_less_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
   3.203 +lemma mset_subset_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
   3.204  proof (induct A arbitrary: B)
   3.205    case (empty M)
   3.206 -  then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
   3.207 +  then have "M \<noteq> {#}" by (simp add: mset_subset_empty_nonempty)
   3.208    then obtain M' x where "M = M' + {#x#}"
   3.209      by (blast dest: multi_nonempty_split)
   3.210    then show ?case by simp
   3.211 @@ -1000,11 +997,11 @@
   3.212    have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
   3.213    have SxsubT: "S + {#x#} \<subset># T" by fact
   3.214    then have "x \<in># T" and "S \<subset># T"
   3.215 -    by (auto dest: mset_less_insertD)
   3.216 +    by (auto dest: mset_subset_insertD)
   3.217    then obtain T' where T: "T = T' + {#x#}"
   3.218      by (blast dest: multi_member_split)
   3.219    then have "S \<subset># T'" using SxsubT
   3.220 -    by (blast intro: mset_less_add_bothsides)
   3.221 +    by (blast intro: mset_subset_add_bothsides)
   3.222    then have "size S < size T'" using IH by simp
   3.223    then show ?case using T by simp
   3.224  qed
   3.225 @@ -1017,15 +1014,15 @@
   3.226  
   3.227  text \<open>Well-foundedness of strict subset relation\<close>
   3.228  
   3.229 -lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
   3.230 +lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
   3.231  apply (rule wf_measure [THEN wf_subset, where f1=size])
   3.232 -apply (clarsimp simp: measure_def inv_image_def mset_less_size)
   3.233 +apply (clarsimp simp: measure_def inv_image_def mset_subset_size)
   3.234  done
   3.235  
   3.236  lemma full_multiset_induct [case_names less]:
   3.237  assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
   3.238  shows "P B"
   3.239 -apply (rule wf_less_mset_rel [THEN wf_induct])
   3.240 +apply (rule wf_subset_mset_rel [THEN wf_induct])
   3.241  apply (rule ih, auto)
   3.242  done
   3.243  
   3.244 @@ -1044,8 +1041,8 @@
   3.245      assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
   3.246      show "P (F + {#x#})"
   3.247      proof (rule insert)
   3.248 -      from i show "x \<in># A" by (auto dest: mset_le_insertD)
   3.249 -      from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
   3.250 +      from i show "x \<in># A" by (auto dest: mset_subset_eq_insertD)
   3.251 +      from i have "F \<subseteq># A" by (auto dest: mset_subset_eq_insertD)
   3.252        with P show "P F" .
   3.253      qed
   3.254    qed
   3.255 @@ -1540,8 +1537,8 @@
   3.256  lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   3.257    by (induct n, simp_all)
   3.258  
   3.259 -lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
   3.260 -  by (auto simp add: mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
   3.261 +lemma count_le_replicate_mset_subset_eq: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
   3.262 +  by (auto simp add: mset_subset_eqI) (metis count_replicate_mset subseteq_mset_def)
   3.263  
   3.264  lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
   3.265    by (induct D) simp_all
   3.266 @@ -1914,7 +1911,7 @@
   3.267  
   3.268  hide_const (open) part
   3.269  
   3.270 -lemma mset_remdups_le: "mset (remdups xs) \<subseteq># mset xs"
   3.271 +lemma mset_remdups_subset_eq: "mset (remdups xs) \<subseteq># mset xs"
   3.272    by (induct xs) (auto intro: subset_mset.order_trans)
   3.273  
   3.274  lemma mset_update:
   3.275 @@ -1934,8 +1931,8 @@
   3.276        apply (subst add.commute [of "{#v#}" "{#x#}"])
   3.277        apply (subst add.assoc [symmetric])
   3.278        apply simp
   3.279 -      apply (rule mset_le_multiset_union_diff_commute)
   3.280 -      apply (simp add: mset_le_single nth_mem_mset)
   3.281 +      apply (rule mset_subset_eq_multiset_union_diff_commute)
   3.282 +      apply (simp add: mset_subset_eq_single nth_mem_mset)
   3.283        done
   3.284    qed
   3.285  qed
   3.286 @@ -2524,7 +2521,7 @@
   3.287  lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
   3.288    by (fact add_left_imp_eq)
   3.289  
   3.290 -lemma mset_less_trans: "(M::'a multiset) \<subset># K \<Longrightarrow> K \<subset># N \<Longrightarrow> M \<subset># N"
   3.291 +lemma mset_subset_trans: "(M::'a multiset) \<subset># K \<Longrightarrow> K \<subset># N \<Longrightarrow> M \<subset># N"
   3.292    by (fact subset_mset.less_trans)
   3.293  
   3.294  lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
   3.295 @@ -2650,18 +2647,18 @@
   3.296  
   3.297  declare size_mset [code]
   3.298  
   3.299 -fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   3.300 -  "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
   3.301 -| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of
   3.302 +fun subset_eq_mset_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   3.303 +  "subset_eq_mset_impl [] ys = Some (ys \<noteq> [])"
   3.304 +| "subset_eq_mset_impl (Cons x xs) ys = (case List.extract (op = x) ys of
   3.305       None \<Rightarrow> None
   3.306 -   | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
   3.307 -
   3.308 -lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<subseteq># mset ys) \<and>
   3.309 -  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> mset xs \<subset># mset ys) \<and>
   3.310 -  (ms_lesseq_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
   3.311 +   | Some (ys1,_,ys2) \<Rightarrow> subset_eq_mset_impl xs (ys1 @ ys2))"
   3.312 +
   3.313 +lemma subset_eq_mset_impl: "(subset_eq_mset_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<subseteq># mset ys) \<and>
   3.314 +  (subset_eq_mset_impl xs ys = Some True \<longleftrightarrow> mset xs \<subset># mset ys) \<and>
   3.315 +  (subset_eq_mset_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
   3.316  proof (induct xs arbitrary: ys)
   3.317    case (Nil ys)
   3.318 -  show ?case by (auto simp: mset_less_empty_nonempty)
   3.319 +  show ?case by (auto simp: mset_subset_empty_nonempty)
   3.320  next
   3.321    case (Cons x xs ys)
   3.322    show ?case
   3.323 @@ -2686,7 +2683,7 @@
   3.324      from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
   3.325      hence id: "mset ys = mset (ys1 @ ys2) + {#x#}"
   3.326        by (auto simp: ac_simps)
   3.327 -    show ?thesis unfolding ms_lesseq_impl.simps
   3.328 +    show ?thesis unfolding subset_eq_mset_impl.simps
   3.329        unfolding Some option.simps split
   3.330        unfolding id
   3.331        using Cons[of "ys1 @ ys2"]
   3.332 @@ -2694,20 +2691,20 @@
   3.333    qed
   3.334  qed
   3.335  
   3.336 -lemma [code]: "mset xs \<subseteq># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   3.337 -  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   3.338 -
   3.339 -lemma [code]: "mset xs \<subset># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   3.340 -  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   3.341 +lemma [code]: "mset xs \<subseteq># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys \<noteq> None"
   3.342 +  using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
   3.343 +
   3.344 +lemma [code]: "mset xs \<subset># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys = Some True"
   3.345 +  using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
   3.346  
   3.347  instantiation multiset :: (equal) equal
   3.348  begin
   3.349  
   3.350  definition
   3.351    [code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
   3.352 -lemma [code]: "HOL.equal (mset xs) (mset ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
   3.353 +lemma [code]: "HOL.equal (mset xs) (mset ys) \<longleftrightarrow> subset_eq_mset_impl xs ys = Some False"
   3.354    unfolding equal_multiset_def
   3.355 -  using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   3.356 +  using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
   3.357  
   3.358  instance
   3.359    by standard (simp add: equal_multiset_def)
     4.1 --- a/src/HOL/Library/Multiset_Order.thy	Thu Jun 16 17:11:00 2016 +0200
     4.2 +++ b/src/HOL/Library/Multiset_Order.thy	Fri Jun 17 12:37:43 2016 +0200
     4.3 @@ -277,14 +277,14 @@
     4.4  lemma less_multiset_empty_right[simp]:
     4.5    fixes M :: "('a :: linorder) multiset"
     4.6    shows "\<not> M #\<subset># {#}"
     4.7 -  using le_empty less_multiset\<^sub>D\<^sub>M by blast
     4.8 +  using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast
     4.9  
    4.10  lemma
    4.11    fixes M N :: "('a :: linorder) multiset"
    4.12    shows
    4.13      le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and
    4.14      le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)"
    4.15 -  using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
    4.16 +  using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
    4.17  
    4.18  lemma
    4.19    fixes M N :: "('a :: linorder) multiset"
     5.1 --- a/src/HOL/Library/Permutation.thy	Thu Jun 16 17:11:00 2016 +0200
     5.2 +++ b/src/HOL/Library/Permutation.thy	Fri Jun 17 12:37:43 2016 +0200
     5.3 @@ -135,7 +135,7 @@
     5.4    done
     5.5  
     5.6  proposition mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     5.7 -  apply (auto simp: mset_eq_perm[THEN sym] mset_le_exists_conv)
     5.8 +  apply (auto simp: mset_eq_perm[THEN sym] mset_subset_eq_exists_conv)
     5.9    apply (insert surj_mset)
    5.10    apply (drule surjD)
    5.11    apply (blast intro: sym)+