Renaming multiset operators < ~> <#,...
authorMathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
Wed Jun 10 13:24:16 2015 +0200 (2015-06-10)
changeset 60397f8a513fedb31
parent 60393 b640770117fd
child 60398 ee390872389a
Renaming multiset operators < ~> <#,...
NEWS
src/HOL/Algebra/Divisibility.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/Library/Permutation.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/UNITY/Follows.thy
     1.1 --- a/NEWS	Mon Jun 08 22:04:19 2015 +0200
     1.2 +++ b/NEWS	Wed Jun 10 13:24:16 2015 +0200
     1.3 @@ -47,6 +47,24 @@
     1.4  separate constants, and infix syntax is usually not available during
     1.5  instantiation.
     1.6  
     1.7 +* Library/Multiset:
     1.8 +  - Renamed multiset inclusion operators:
     1.9 +      < ~> <#
    1.10 +      \<subset> ~> \<subset>#
    1.11 +      <= ~> <=#
    1.12 +      \<le> ~> \<le>#
    1.13 +      \<subseteq> ~> \<subseteq>#
    1.14 +    INCOMPATIBILITY.
    1.15 +  - "'a multiset" is no longer an instance of the "order",
    1.16 +    "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
    1.17 +    "semilattice_inf", and "semilattice_sup" type classes. The theorems
    1.18 +    previously provided by these type classes (directly or indirectly)
    1.19 +    are now available through the "subset_mset" interpretation
    1.20 +    (e.g. add_mono ~> subset_mset.add_mono).
    1.21 +    INCOMPATIBILITY.
    1.22 +  - Removing mset_le_def:
    1.23 +    mset_le_def ~> subseteq_mset_def
    1.24 +    mset_less_def ~> subset_mset_def
    1.25  
    1.26  New in Isabelle2015 (May 2015)
    1.27  ------------------------------
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Mon Jun 08 22:04:19 2015 +0200
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 10 13:24:16 2015 +0200
     2.3 @@ -2137,7 +2137,7 @@
     2.4    assumes ab: "a divides b"
     2.5      and afs: "wfactors G as a" and bfs: "wfactors G bs b"
     2.6      and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
     2.7 -  shows "fmset G as \<le> fmset G bs"
     2.8 +  shows "fmset G as \<le># fmset G bs"
     2.9  using ab
    2.10  proof (elim dividesE)
    2.11    fix c
    2.12 @@ -2157,7 +2157,7 @@
    2.13  qed
    2.14  
    2.15  lemma (in comm_monoid_cancel) fmsubset_divides:
    2.16 -  assumes msubset: "fmset G as \<le> fmset G bs"
    2.17 +  assumes msubset: "fmset G as \<le># fmset G bs"
    2.18      and afs: "wfactors G as a" and bfs: "wfactors G bs b"
    2.19      and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
    2.20      and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
    2.21 @@ -2193,7 +2193,7 @@
    2.22  
    2.23    from csmset msubset
    2.24        have "fmset G bs = fmset G as + fmset G cs"
    2.25 -      by (simp add: multiset_eq_iff mset_le_def)
    2.26 +      by (simp add: multiset_eq_iff subseteq_mset_def)
    2.27    hence basc: "b \<sim> a \<otimes> c"
    2.28        by (rule fmset_wfactors_mult) fact+
    2.29  
    2.30 @@ -2210,7 +2210,7 @@
    2.31    assumes "wfactors G as a" and "wfactors G bs b"
    2.32      and "a \<in> carrier G" and "b \<in> carrier G" 
    2.33      and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
    2.34 -  shows "a divides b = (fmset G as \<le> fmset G bs)"
    2.35 +  shows "a divides b = (fmset G as \<le># fmset G bs)"
    2.36  using assms
    2.37  by (blast intro: divides_fmsubset fmsubset_divides)
    2.38  
    2.39 @@ -2218,7 +2218,7 @@
    2.40  text {* Proper factors on multisets *}
    2.41  
    2.42  lemma (in factorial_monoid) fmset_properfactor:
    2.43 -  assumes asubb: "fmset G as \<le> fmset G bs"
    2.44 +  assumes asubb: "fmset G as \<le># fmset G bs"
    2.45      and anb: "fmset G as \<noteq> fmset G bs"
    2.46      and "wfactors G as a" and "wfactors G bs b"
    2.47      and "a \<in> carrier G" and "b \<in> carrier G"
    2.48 @@ -2228,10 +2228,10 @@
    2.49  apply (rule fmsubset_divides[of as bs], fact+)
    2.50  proof
    2.51    assume "b divides a"
    2.52 -  hence "fmset G bs \<le> fmset G as"
    2.53 +  hence "fmset G bs \<le># fmset G as"
    2.54        by (rule divides_fmsubset) fact+
    2.55    with asubb
    2.56 -      have "fmset G as = fmset G bs" by (rule order_antisym)
    2.57 +      have "fmset G as = fmset G bs" by (rule subset_mset.antisym)
    2.58    with anb
    2.59        show "False" ..
    2.60  qed
    2.61 @@ -2241,7 +2241,7 @@
    2.62      and "wfactors G as a" and "wfactors G bs b"
    2.63      and "a \<in> carrier G" and "b \<in> carrier G"
    2.64      and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
    2.65 -  shows "fmset G as \<le> fmset G bs \<and> fmset G as \<noteq> fmset G bs"
    2.66 +  shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
    2.67  using pf
    2.68  apply (elim properfactorE)
    2.69  apply rule
    2.70 @@ -2619,13 +2619,13 @@
    2.71    have "c gcdof a b"
    2.72    proof (simp add: isgcd_def, safe)
    2.73      from csmset
    2.74 -        have "fmset G cs \<le> fmset G as"
    2.75 -        by (simp add: multiset_inter_def mset_le_def)
    2.76 +        have "fmset G cs \<le># fmset G as"
    2.77 +        by (simp add: multiset_inter_def subset_mset_def)
    2.78      thus "c divides a" by (rule fmsubset_divides) fact+
    2.79    next
    2.80      from csmset
    2.81 -        have "fmset G cs \<le> fmset G bs"
    2.82 -        by (simp add: multiset_inter_def mset_le_def, force)
    2.83 +        have "fmset G cs \<le># fmset G bs"
    2.84 +        by (simp add: multiset_inter_def subseteq_mset_def, force)
    2.85      thus "c divides b" by (rule fmsubset_divides) fact+
    2.86    next
    2.87      fix y
    2.88 @@ -2637,13 +2637,13 @@
    2.89          by auto
    2.90  
    2.91      assume "y divides a"
    2.92 -    hence ya: "fmset G ys \<le> fmset G as" by (rule divides_fmsubset) fact+
    2.93 +    hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+
    2.94  
    2.95      assume "y divides b"
    2.96 -    hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
    2.97 +    hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+
    2.98  
    2.99      from ya yb csmset
   2.100 -    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
   2.101 +    have "fmset G ys \<le># fmset G cs" by (simp add: subset_mset_def)
   2.102      thus "y divides c" by (rule fmsubset_divides) fact+
   2.103    qed
   2.104  
   2.105 @@ -2718,10 +2718,10 @@
   2.106  
   2.107    have "c lcmof a b"
   2.108    proof (simp add: islcm_def, safe)
   2.109 -    from csmset have "fmset G as \<le> fmset G cs" by (simp add: mset_le_def, force)
   2.110 +    from csmset have "fmset G as \<le># fmset G cs" by (simp add: subseteq_mset_def, force)
   2.111      thus "a divides c" by (rule fmsubset_divides) fact+
   2.112    next
   2.113 -    from csmset have "fmset G bs \<le> fmset G cs" by (simp add: mset_le_def)
   2.114 +    from csmset have "fmset G bs \<le># fmset G cs" by (simp add: subset_mset_def)
   2.115      thus "b divides c" by (rule fmsubset_divides) fact+
   2.116    next
   2.117      fix y
   2.118 @@ -2733,14 +2733,14 @@
   2.119          by auto
   2.120  
   2.121      assume "a divides y"
   2.122 -    hence ya: "fmset G as \<le> fmset G ys" by (rule divides_fmsubset) fact+
   2.123 +    hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+
   2.124  
   2.125      assume "b divides y"
   2.126 -    hence yb: "fmset G bs \<le> fmset G ys" by (rule divides_fmsubset) fact+
   2.127 +    hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+
   2.128  
   2.129      from ya yb csmset
   2.130 -    have "fmset G cs \<le> fmset G ys"
   2.131 -      apply (simp add: mset_le_def, clarify)
   2.132 +    have "fmset G cs \<le># fmset G ys"
   2.133 +      apply (simp add: subseteq_mset_def, clarify)
   2.134        apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
   2.135         apply simp
   2.136        apply simp
     3.1 --- a/src/HOL/Library/DAList_Multiset.thy	Mon Jun 08 22:04:19 2015 +0200
     3.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Wed Jun 10 13:24:16 2015 +0200
     3.3 @@ -18,9 +18,9 @@
     3.4  
     3.5  lemma [code, code del]: "minus = (minus :: 'a multiset \<Rightarrow> _)" ..
     3.6  
     3.7 -lemma [code, code del]: "inf = (inf :: 'a multiset \<Rightarrow> _)" ..
     3.8 +lemma [code, code del]: "inf_subset_mset = (inf_subset_mset :: 'a multiset \<Rightarrow> _)" ..
     3.9  
    3.10 -lemma [code, code del]: "sup = (sup :: 'a multiset \<Rightarrow> _)" ..
    3.11 +lemma [code, code del]: "sup_subset_mset = (sup_subset_mset :: 'a multiset \<Rightarrow> _)" ..
    3.12  
    3.13  lemma [code, code del]: "image_mset = image_mset" ..
    3.14  
    3.15 @@ -38,9 +38,9 @@
    3.16  
    3.17  lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
    3.18  
    3.19 -lemma [code, code del]: "ord_multiset_inst.less_eq_multiset = ord_multiset_inst.less_eq_multiset" ..
    3.20 +lemma [code, code del]: "subset_mset = subset_mset" ..
    3.21  
    3.22 -lemma [code, code del]: "ord_multiset_inst.less_multiset = ord_multiset_inst.less_multiset" ..
    3.23 +lemma [code, code del]: "subseteq_mset = subseteq_mset" ..
    3.24  
    3.25  lemma [code, code del]: "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset" ..
    3.26  
    3.27 @@ -203,21 +203,21 @@
    3.28    by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
    3.29  
    3.30  
    3.31 -lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le> m2 \<and> m2 \<le> m1"
    3.32 -  by (metis equal_multiset_def eq_iff)
    3.33 +lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
    3.34 +  by (metis equal_multiset_def subset_mset.eq_iff)
    3.35  
    3.36  text \<open>By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
    3.37  With equality implemented by @{text"\<le>"}, this leads to three calls of  @{text"\<le>"}.
    3.38  Here is a more efficient version:\<close>
    3.39 -lemma mset_less[code]: "xs < (ys :: 'a multiset) \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    3.40 -  by (rule less_le_not_le)
    3.41 +lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
    3.42 +  by (rule subset_mset.less_le_not_le)
    3.43  
    3.44  lemma mset_less_eq_Bag0:
    3.45 -  "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)"
    3.46 +  "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)"
    3.47      (is "?lhs \<longleftrightarrow> ?rhs")
    3.48  proof
    3.49    assume ?lhs
    3.50 -  then show ?rhs by (auto simp add: mset_le_def)
    3.51 +  then show ?rhs by (auto simp add: subseteq_mset_def)
    3.52  next
    3.53    assume ?rhs
    3.54    show ?lhs
    3.55 @@ -225,12 +225,12 @@
    3.56      fix x
    3.57      from \<open>?rhs\<close> have "count_of (DAList.impl_of xs) x \<le> count A x"
    3.58        by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
    3.59 -    then show "count (Bag xs) x \<le> count A x" by (simp add: mset_le_def)
    3.60 +    then show "count (Bag xs) x \<le> count A x" by (simp add: subset_mset_def)
    3.61    qed
    3.62  qed
    3.63  
    3.64  lemma mset_less_eq_Bag [code]:
    3.65 -  "Bag xs \<le> (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
    3.66 +  "Bag xs \<le># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
    3.67  proof -
    3.68    {
    3.69      fix x n
    3.70 @@ -266,7 +266,7 @@
    3.71  qed
    3.72  
    3.73  declare multiset_inter_def [code]
    3.74 -declare sup_multiset_def [code]
    3.75 +declare sup_subset_mset_def [code]
    3.76  declare multiset_of.simps [code]
    3.77  
    3.78  
     4.1 --- a/src/HOL/Library/Multiset.thy	Mon Jun 08 22:04:19 2015 +0200
     4.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 10 13:24:16 2015 +0200
     4.3 @@ -280,157 +280,137 @@
     4.4  
     4.5  subsubsection {* Pointwise ordering induced by count *}
     4.6  
     4.7 -instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
     4.8 -begin
     4.9 -
    4.10 -lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
    4.11 -
    4.12 -lemmas mset_le_def = less_eq_multiset_def
    4.13 -
    4.14 -definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    4.15 -  mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
    4.16 -
    4.17 -instance
    4.18 -  by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
    4.19 -
    4.20 -end
    4.21 -
    4.22 -abbreviation less_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
    4.23 -  "A <# B \<equiv> A < B"
    4.24 -abbreviation (xsymbols) subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
    4.25 -  "A \<subset># B \<equiv> A < B"
    4.26 -
    4.27 -abbreviation less_eq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
    4.28 -  "A <=# B \<equiv> A \<le> B"
    4.29 -abbreviation (xsymbols) leq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
    4.30 -  "A \<le># B \<equiv> A \<le> B"
    4.31 -abbreviation (xsymbols) subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
    4.32 -  "A \<subseteq># B \<equiv> A \<le> B"
    4.33 +definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
    4.34 +"subseteq_mset A B \<equiv> (\<forall>a. count A a \<le> count B a)"
    4.35 +
    4.36 +definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
    4.37 +"subset_mset A B \<equiv> (A <=# B \<and> A \<noteq> B)"
    4.38 +
    4.39 +notation subseteq_mset (infix "\<le>#" 50)
    4.40 +notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)
    4.41 +
    4.42 +notation (xsymbols) subset_mset (infix "\<subset>#" 50)
    4.43 +
    4.44 +interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op <=#" "op <#"
    4.45 +  by default (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
    4.46  
    4.47  lemma mset_less_eqI:
    4.48 -  "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B"
    4.49 -  by (simp add: mset_le_def)
    4.50 +  "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le># B"
    4.51 +  by (simp add: subseteq_mset_def)
    4.52  
    4.53  lemma mset_le_exists_conv:
    4.54 -  "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
    4.55 -apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
    4.56 +  "(A::'a multiset) \<le># B \<longleftrightarrow> (\<exists>C. B = A + C)"
    4.57 +apply (unfold subseteq_mset_def, rule iffI, rule_tac x = "B - A" in exI)
    4.58  apply (auto intro: multiset_eq_iff [THEN iffD2])
    4.59  done
    4.60  
    4.61 -instance multiset :: (type) ordered_cancel_comm_monoid_diff
    4.62 +interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" "op -" 0 "op \<le>#" "op <#"
    4.63    by default (simp, fact mset_le_exists_conv)
    4.64  
    4.65  lemma mset_le_mono_add_right_cancel [simp]:
    4.66 -  "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
    4.67 -  by (fact add_le_cancel_right)
    4.68 +  "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
    4.69 +  by (fact subset_mset.add_le_cancel_right)
    4.70  
    4.71  lemma mset_le_mono_add_left_cancel [simp]:
    4.72 -  "C + (A::'a multiset) \<le> C + B \<longleftrightarrow> A \<le> B"
    4.73 -  by (fact add_le_cancel_left)
    4.74 +  "C + (A::'a multiset) \<le># C + B \<longleftrightarrow> A \<le># B"
    4.75 +  by (fact subset_mset.add_le_cancel_left)
    4.76  
    4.77  lemma mset_le_mono_add:
    4.78 -  "(A::'a multiset) \<le> B \<Longrightarrow> C \<le> D \<Longrightarrow> A + C \<le> B + D"
    4.79 -  by (fact add_mono)
    4.80 +  "(A::'a multiset) \<le># B \<Longrightarrow> C \<le># D \<Longrightarrow> A + C \<le># B + D"
    4.81 +  by (fact subset_mset.add_mono)
    4.82  
    4.83  lemma mset_le_add_left [simp]:
    4.84 -  "(A::'a multiset) \<le> A + B"
    4.85 -  unfolding mset_le_def by auto
    4.86 +  "(A::'a multiset) \<le># A + B"
    4.87 +  unfolding subseteq_mset_def by auto
    4.88  
    4.89  lemma mset_le_add_right [simp]:
    4.90 -  "B \<le> (A::'a multiset) + B"
    4.91 -  unfolding mset_le_def by auto
    4.92 +  "B \<le># (A::'a multiset) + B"
    4.93 +  unfolding subseteq_mset_def by auto
    4.94  
    4.95  lemma mset_le_single:
    4.96 -  "a :# B \<Longrightarrow> {#a#} \<le> B"
    4.97 -  by (simp add: mset_le_def)
    4.98 +  "a :# B \<Longrightarrow> {#a#} \<le># B"
    4.99 +  by (simp add: subseteq_mset_def)
   4.100  
   4.101  lemma multiset_diff_union_assoc:
   4.102 -  "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
   4.103 -  by (simp add: multiset_eq_iff mset_le_def)
   4.104 +  "C \<le># B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
   4.105 +  by (simp add: subset_mset.diff_add_assoc)
   4.106  
   4.107  lemma mset_le_multiset_union_diff_commute:
   4.108 -  "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
   4.109 -by (simp add: multiset_eq_iff mset_le_def)
   4.110 -
   4.111 -lemma diff_le_self[simp]: "(M::'a multiset) - N \<le> M"
   4.112 -by(simp add: mset_le_def)
   4.113 -
   4.114 -lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   4.115 -apply (clarsimp simp: mset_le_def mset_less_def)
   4.116 +  "B \<le># A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
   4.117 +by (simp add: subset_mset.add_diff_assoc2)
   4.118 +
   4.119 +lemma diff_le_self[simp]: "(M::'a multiset) - N \<le># M"
   4.120 +by(simp add: subseteq_mset_def)
   4.121 +
   4.122 +lemma mset_lessD: "A <# B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   4.123 +apply (clarsimp simp: subset_mset_def subseteq_mset_def)
   4.124  apply (erule_tac x=x in allE)
   4.125  apply auto
   4.126  done
   4.127  
   4.128 -lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   4.129 -apply (clarsimp simp: mset_le_def mset_less_def)
   4.130 +lemma mset_leD: "A \<le># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   4.131 +apply (clarsimp simp: subset_mset_def subseteq_mset_def)
   4.132  apply (erule_tac x = x in allE)
   4.133  apply auto
   4.134  done
   4.135  
   4.136 -lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)"
   4.137 +lemma mset_less_insertD: "(A + {#x#} <# B) \<Longrightarrow> (x \<in># B \<and> A <# B)"
   4.138  apply (rule conjI)
   4.139   apply (simp add: mset_lessD)
   4.140 -apply (clarsimp simp: mset_le_def mset_less_def)
   4.141 +apply (clarsimp simp: subset_mset_def subseteq_mset_def)
   4.142  apply safe
   4.143   apply (erule_tac x = a in allE)
   4.144   apply (auto split: split_if_asm)
   4.145  done
   4.146  
   4.147 -lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> B)"
   4.148 +lemma mset_le_insertD: "(A + {#x#} \<le># B) \<Longrightarrow> (x \<in># B \<and> A \<le># B)"
   4.149  apply (rule conjI)
   4.150   apply (simp add: mset_leD)
   4.151 -apply (force simp: mset_le_def mset_less_def split: split_if_asm)
   4.152 +apply (force simp: subset_mset_def subseteq_mset_def split: split_if_asm)
   4.153  done
   4.154  
   4.155 -lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
   4.156 -  by (auto simp add: mset_less_def mset_le_def multiset_eq_iff)
   4.157 -
   4.158 -lemma empty_le[simp]: "{#} \<le> A"
   4.159 +lemma mset_less_of_empty[simp]: "A <# {#} \<longleftrightarrow> False"
   4.160 +  by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff)
   4.161 +
   4.162 +lemma empty_le[simp]: "{#} \<le># A"
   4.163    unfolding mset_le_exists_conv by auto
   4.164  
   4.165 -lemma le_empty[simp]: "(M \<le> {#}) = (M = {#})"
   4.166 +lemma le_empty[simp]: "(M \<le># {#}) = (M = {#})"
   4.167    unfolding mset_le_exists_conv by auto
   4.168  
   4.169 -lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
   4.170 -  by (auto simp: mset_le_def mset_less_def)
   4.171 -
   4.172 -lemma multi_psub_self[simp]: "(A::'a multiset) < A = False"
   4.173 +lemma multi_psub_of_add_self[simp]: "A <# A + {#x#}"
   4.174 +  by (auto simp: subset_mset_def subseteq_mset_def)
   4.175 +
   4.176 +lemma multi_psub_self[simp]: "(A::'a multiset) <# A = False"
   4.177    by simp
   4.178  
   4.179 -lemma mset_less_add_bothsides: "N + {#x#} < M + {#x#} \<Longrightarrow> N < M"
   4.180 -  by (fact add_less_imp_less_right)
   4.181 +lemma mset_less_add_bothsides: "N + {#x#} <# M + {#x#} \<Longrightarrow> N <# M"
   4.182 +  by (fact subset_mset.add_less_imp_less_right)
   4.183  
   4.184  lemma mset_less_empty_nonempty:
   4.185 -  "{#} < S \<longleftrightarrow> S \<noteq> {#}"
   4.186 -  by (auto simp: mset_le_def mset_less_def)
   4.187 +  "{#} <# S \<longleftrightarrow> S \<noteq> {#}"
   4.188 +  by (auto simp: subset_mset_def subseteq_mset_def)
   4.189  
   4.190  lemma mset_less_diff_self:
   4.191 -  "c \<in># B \<Longrightarrow> B - {#c#} < B"
   4.192 -  by (auto simp: mset_le_def mset_less_def multiset_eq_iff)
   4.193 +  "c \<in># B \<Longrightarrow> B - {#c#} <# B"
   4.194 +  by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff)
   4.195  
   4.196  
   4.197  subsubsection {* Intersection *}
   4.198  
   4.199 -instantiation multiset :: (type) semilattice_inf
   4.200 -begin
   4.201 -
   4.202 -definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   4.203 -  multiset_inter_def: "inf_multiset A B = A - (A - B)"
   4.204 -
   4.205 -instance
   4.206 +definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
   4.207 +  multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
   4.208 +
   4.209 +interpretation subset_mset: semilattice_inf inf_subset_mset "op \<le>#" "op <#"
   4.210  proof -
   4.211 -  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
   4.212 -  show "OFCLASS('a multiset, semilattice_inf_class)"
   4.213 -    by default (auto simp add: multiset_inter_def mset_le_def aux)
   4.214 +   have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
   4.215 +   show "class.semilattice_inf op #\<inter> op \<le># op <#"
   4.216 +     by default (auto simp add: multiset_inter_def subseteq_mset_def aux)
   4.217  qed
   4.218  
   4.219 -end
   4.220 -
   4.221 -abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
   4.222 -  "multiset_inter \<equiv> inf"
   4.223  
   4.224  lemma multiset_inter_count [simp]:
   4.225 -  "count (A #\<inter> B) x = min (count A x) (count B x)"
   4.226 +  "count ((A::'a multiset) #\<inter> B) x = min (count A x) (count B x)"
   4.227    by (simp add: multiset_inter_def)
   4.228  
   4.229  lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   4.230 @@ -475,28 +455,19 @@
   4.231  
   4.232  
   4.233  subsubsection {* Bounded union *}
   4.234 -
   4.235 -instantiation multiset :: (type) semilattice_sup
   4.236 -begin
   4.237 -
   4.238 -definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   4.239 -  "sup_multiset A B = A + (B - A)"
   4.240 -
   4.241 -instance
   4.242 +definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)  where
   4.243 +  "sup_subset_mset A B = A + (B - A)"
   4.244 +
   4.245 +interpretation subset_mset: semilattice_sup sup_subset_mset "op \<le>#" "op <#"
   4.246  proof -
   4.247    have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
   4.248 -  show "OFCLASS('a multiset, semilattice_sup_class)"
   4.249 -    by default (auto simp add: sup_multiset_def mset_le_def aux)
   4.250 +  show "class.semilattice_sup op #\<union> op \<le># op <#"
   4.251 +    by default (auto simp add: sup_subset_mset_def subseteq_mset_def aux)
   4.252  qed
   4.253  
   4.254 -end
   4.255 -
   4.256 -abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where
   4.257 -  "sup_multiset \<equiv> sup"
   4.258 -
   4.259 -lemma sup_multiset_count [simp]:
   4.260 +lemma sup_subset_mset_count [simp]:
   4.261    "count (A #\<union> B) x = max (count A x) (count B x)"
   4.262 -  by (simp add: sup_multiset_def)
   4.263 +  by (simp add: sup_subset_mset_def)
   4.264  
   4.265  lemma empty_sup [simp]:
   4.266    "{#} #\<union> M = M"
   4.267 @@ -522,6 +493,8 @@
   4.268    "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
   4.269    by (simp add: multiset_eq_iff)
   4.270  
   4.271 +subsubsection {*Subset is an order*}
   4.272 +interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
   4.273  
   4.274  subsubsection {* Filter (with comprehension syntax) *}
   4.275  
   4.276 @@ -555,11 +528,11 @@
   4.277    "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
   4.278    by (rule multiset_eqI) simp
   4.279  
   4.280 -lemma multiset_filter_subset[simp]: "filter_mset f M \<le> M"
   4.281 -  unfolding less_eq_multiset.rep_eq by auto
   4.282 -
   4.283 -lemma multiset_filter_mono: assumes "A \<le> B"
   4.284 -  shows "filter_mset f A \<le> filter_mset f B"
   4.285 +lemma multiset_filter_subset[simp]: "filter_mset f M \<le># M"
   4.286 +  by (simp add: mset_less_eqI)
   4.287 +
   4.288 +lemma multiset_filter_mono: assumes "A \<le># B"
   4.289 +  shows "filter_mset f A \<le># filter_mset f B"
   4.290  proof -
   4.291    from assms[unfolded mset_le_exists_conv]
   4.292    obtain C where B: "B = A + C" by auto
   4.293 @@ -603,7 +576,7 @@
   4.294  lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
   4.295    unfolding set_of_def[symmetric] by simp
   4.296  
   4.297 -lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
   4.298 +lemma set_of_mono: "A \<le># B \<Longrightarrow> set_of A \<subseteq> set_of B"
   4.299    by (metis mset_leD subsetI mem_set_of_iff)
   4.300  
   4.301  lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
   4.302 @@ -685,7 +658,7 @@
   4.303    then show ?thesis by blast
   4.304  qed
   4.305  
   4.306 -lemma size_mset_mono: assumes "A \<le> B"
   4.307 +lemma size_mset_mono: assumes "A \<le># B"
   4.308    shows "size A \<le> size(B::_ multiset)"
   4.309  proof -
   4.310    from assms[unfolded mset_le_exists_conv]
   4.311 @@ -697,7 +670,7 @@
   4.312  by (rule size_mset_mono[OF multiset_filter_subset])
   4.313  
   4.314  lemma size_Diff_submset:
   4.315 -  "M \<le> M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
   4.316 +  "M \<le># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
   4.317  by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
   4.318  
   4.319  subsection {* Induction and case splits *}
   4.320 @@ -732,7 +705,7 @@
   4.321  apply auto
   4.322  done
   4.323  
   4.324 -lemma mset_less_size: "(A::'a multiset) < B \<Longrightarrow> size A < size B"
   4.325 +lemma mset_less_size: "(A::'a multiset) <# B \<Longrightarrow> size A < size B"
   4.326  proof (induct A arbitrary: B)
   4.327    case (empty M)
   4.328    then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
   4.329 @@ -741,12 +714,12 @@
   4.330    then show ?case by simp
   4.331  next
   4.332    case (add S x T)
   4.333 -  have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact
   4.334 -  have SxsubT: "S + {#x#} < T" by fact
   4.335 -  then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD)
   4.336 +  have IH: "\<And>B. S <# B \<Longrightarrow> size S < size B" by fact
   4.337 +  have SxsubT: "S + {#x#} <# T" by fact
   4.338 +  then have "x \<in># T" and "S <# T" by (auto dest: mset_less_insertD)
   4.339    then obtain T' where T: "T = T' + {#x#}"
   4.340      by (blast dest: multi_member_split)
   4.341 -  then have "S < T'" using SxsubT
   4.342 +  then have "S <# T'" using SxsubT
   4.343      by (blast intro: mset_less_add_bothsides)
   4.344    then have "size S < size T'" using IH by simp
   4.345    then show ?case using T by simp
   4.346 @@ -760,35 +733,35 @@
   4.347  
   4.348  text {* Well-foundedness of strict subset relation *}
   4.349  
   4.350 -lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}"
   4.351 +lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M <# N}"
   4.352  apply (rule wf_measure [THEN wf_subset, where f1=size])
   4.353  apply (clarsimp simp: measure_def inv_image_def mset_less_size)
   4.354  done
   4.355  
   4.356  lemma full_multiset_induct [case_names less]:
   4.357 -assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B"
   4.358 +assumes ih: "\<And>B. \<forall>(A::'a multiset). A <# B \<longrightarrow> P A \<Longrightarrow> P B"
   4.359  shows "P B"
   4.360  apply (rule wf_less_mset_rel [THEN wf_induct])
   4.361  apply (rule ih, auto)
   4.362  done
   4.363  
   4.364  lemma multi_subset_induct [consumes 2, case_names empty add]:
   4.365 -assumes "F \<le> A"
   4.366 +assumes "F \<le># A"
   4.367    and empty: "P {#}"
   4.368    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
   4.369  shows "P F"
   4.370  proof -
   4.371 -  from `F \<le> A`
   4.372 +  from `F \<le># A`
   4.373    show ?thesis
   4.374    proof (induct F)
   4.375      show "P {#}" by fact
   4.376    next
   4.377      fix x F
   4.378 -    assume P: "F \<le> A \<Longrightarrow> P F" and i: "F + {#x#} \<le> A"
   4.379 +    assume P: "F \<le># A \<Longrightarrow> P F" and i: "F + {#x#} \<le># A"
   4.380      show "P (F + {#x#})"
   4.381      proof (rule insert)
   4.382        from i show "x \<in># A" by (auto dest: mset_le_insertD)
   4.383 -      from i have "F \<le> A" by (auto dest: mset_le_insertD)
   4.384 +      from i have "F \<le># A" by (auto dest: mset_le_insertD)
   4.385        with P show "P F" .
   4.386      qed
   4.387    qed
   4.388 @@ -1280,8 +1253,8 @@
   4.389  
   4.390  lemma msetsum_diff:
   4.391    fixes M N :: "('a \<Colon> ordered_cancel_comm_monoid_diff) multiset"
   4.392 -  shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
   4.393 -  by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
   4.394 +  shows "N \<le># M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
   4.395 +  by (metis add_diff_cancel_right' msetsum.union subset_mset.diff_add)
   4.396  
   4.397  lemma size_eq_msetsum: "size M = msetsum (image_mset (\<lambda>_. 1) M)"
   4.398  proof (induct M)
   4.399 @@ -1404,8 +1377,9 @@
   4.400  lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   4.401    by (induct n, simp_all)
   4.402  
   4.403 -lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le> M"
   4.404 -  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset less_eq_multiset.rep_eq)
   4.405 +lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># M"
   4.406 +  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
   4.407 +
   4.408  
   4.409  lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
   4.410    by (induct D) simp_all
   4.411 @@ -1555,8 +1529,8 @@
   4.412  
   4.413  hide_const (open) part
   4.414  
   4.415 -lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
   4.416 -  by (induct xs) (auto intro: order_trans)
   4.417 +lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
   4.418 +  by (induct xs) (auto intro: subset_mset.order_trans)
   4.419  
   4.420  lemma multiset_of_update:
   4.421    "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
   4.422 @@ -2037,17 +2011,17 @@
   4.423  lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
   4.424    by (fact add_left_imp_eq)
   4.425  
   4.426 -lemma mset_less_trans: "(M::'a multiset) < K \<Longrightarrow> K < N \<Longrightarrow> M < N"
   4.427 -  by (fact order_less_trans)
   4.428 +lemma mset_less_trans: "(M::'a multiset) <# K \<Longrightarrow> K <# N \<Longrightarrow> M <# N"
   4.429 +  by (fact subset_mset.less_trans)
   4.430  
   4.431  lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
   4.432 -  by (fact inf.commute)
   4.433 +  by (fact subset_mset.inf.commute)
   4.434  
   4.435  lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
   4.436 -  by (fact inf.assoc [symmetric])
   4.437 +  by (fact subset_mset.inf.assoc [symmetric])
   4.438  
   4.439  lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
   4.440 -  by (fact inf.left_commute)
   4.441 +  by (fact subset_mset.inf.left_commute)
   4.442  
   4.443  lemmas multiset_inter_ac =
   4.444    multiset_inter_commute
   4.445 @@ -2182,8 +2156,8 @@
   4.446       None \<Rightarrow> None
   4.447     | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
   4.448  
   4.449 -lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le> multiset_of ys) \<and>
   4.450 -  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs < multiset_of ys) \<and>
   4.451 +lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le># multiset_of ys) \<and>
   4.452 +  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs <# multiset_of ys) \<and>
   4.453    (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
   4.454  proof (induct xs arbitrary: ys)
   4.455    case (Nil ys)
   4.456 @@ -2195,13 +2169,13 @@
   4.457      case None
   4.458      hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
   4.459      {
   4.460 -      assume "multiset_of (x # xs) \<le> multiset_of ys"
   4.461 +      assume "multiset_of (x # xs) \<le># multiset_of ys"
   4.462        from set_of_mono[OF this] x have False by simp
   4.463      } note nle = this
   4.464      moreover
   4.465      {
   4.466 -      assume "multiset_of (x # xs) < multiset_of ys"
   4.467 -      hence "multiset_of (x # xs) \<le> multiset_of ys" by auto
   4.468 +      assume "multiset_of (x # xs) <# multiset_of ys"
   4.469 +      hence "multiset_of (x # xs) \<le># multiset_of ys" by auto
   4.470        from nle[OF this] have False .
   4.471      }
   4.472      ultimately show ?thesis using None by auto
   4.473 @@ -2216,14 +2190,14 @@
   4.474        unfolding Some option.simps split
   4.475        unfolding id
   4.476        using Cons[of "ys1 @ ys2"]
   4.477 -      unfolding mset_le_def mset_less_def by auto
   4.478 +      unfolding subset_mset_def subseteq_mset_def by auto
   4.479    qed
   4.480  qed
   4.481  
   4.482 -lemma [code]: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   4.483 +lemma [code]: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   4.484    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   4.485  
   4.486 -lemma [code]: "multiset_of xs < multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   4.487 +lemma [code]: "multiset_of xs <# multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   4.488    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   4.489  
   4.490  instantiation multiset :: (equal) equal
     5.1 --- a/src/HOL/Library/Multiset_Order.thy	Mon Jun 08 22:04:19 2015 +0200
     5.2 +++ b/src/HOL/Library/Multiset_Order.thy	Wed Jun 10 13:24:16 2015 +0200
     5.3 @@ -69,7 +69,7 @@
     5.4  
     5.5  definition less_multiset\<^sub>D\<^sub>M where
     5.6    "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
     5.7 -   (\<exists>X Y. X \<noteq> {#} \<and> X \<le> N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
     5.8 +   (\<exists>X Y. X \<noteq> {#} \<and> X \<le># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
     5.9  
    5.10  
    5.11  text {* The Huet--Oppen ordering: *}
    5.12 @@ -134,12 +134,12 @@
    5.13  proof -
    5.14    assume "less_multiset\<^sub>D\<^sub>M M N"
    5.15    then obtain X Y where
    5.16 -    "X \<noteq> {#}" and "X \<le> N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    5.17 +    "X \<noteq> {#}" and "X \<le># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    5.18      unfolding less_multiset\<^sub>D\<^sub>M_def by blast
    5.19    then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
    5.20      by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
    5.21 -  with `M = N - X + Y` `X \<le> N` show "(M, N) \<in> mult {(x, y). x < y}"
    5.22 -    by (metis ordered_cancel_comm_monoid_diff_class.diff_add)
    5.23 +  with `M = N - X + Y` `X \<le># N` show "(M, N) \<in> mult {(x, y). x < y}"
    5.24 +    by (metis subset_mset.diff_add)
    5.25  qed
    5.26  
    5.27  lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
    5.28 @@ -151,7 +151,7 @@
    5.29    def X \<equiv> "N - M"
    5.30    def Y \<equiv> "M - N"
    5.31    from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
    5.32 -  from z show "X \<le> N" unfolding X_def by auto
    5.33 +  from z show "X \<le># N" unfolding X_def by auto
    5.34    show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
    5.35    show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
    5.36    proof (intro allI impI)
    5.37 @@ -239,9 +239,9 @@
    5.38  
    5.39  lemma less_eq_imp_le_multiset:
    5.40    fixes M N :: "('a \<Colon> linorder) multiset"
    5.41 -  shows "M \<le> N \<Longrightarrow> M #\<subseteq># N"
    5.42 +  shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
    5.43    unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
    5.44 -  by (auto dest: leD simp add: less_eq_multiset.rep_eq)
    5.45 +  by (simp add: less_le_not_le subseteq_mset_def)
    5.46  
    5.47  lemma less_multiset_right_total:
    5.48    fixes M :: "('a \<Colon> linorder) multiset"
    5.49 @@ -302,7 +302,7 @@
    5.50    unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
    5.51      less_not_sym mset_leD mset_le_add_left)  
    5.52  
    5.53 -lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
    5.54 -  by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
    5.55 +lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
    5.56 +  by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
    5.57  
    5.58  end
     6.1 --- a/src/HOL/Library/Permutation.thy	Mon Jun 08 22:04:19 2015 +0200
     6.2 +++ b/src/HOL/Library/Permutation.thy	Wed Jun 10 13:24:16 2015 +0200
     6.3 @@ -140,7 +140,7 @@
     6.4    apply simp
     6.5    done
     6.6  
     6.7 -lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     6.8 +lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
     6.9    apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
    6.10    apply (insert surj_multiset_of)
    6.11    apply (drule surjD)
     7.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Mon Jun 08 22:04:19 2015 +0200
     7.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jun 10 13:24:16 2015 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  
     7.5  section{*Common Declarations for Chandy and Charpentier's Allocator*}
     7.6  
     7.7 -theory AllocBase imports "../UNITY_Main" begin
     7.8 +theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
     7.9  
    7.10  consts Nclients :: nat  (*Number of clients*)
    7.11  
    7.12 @@ -41,12 +41,19 @@
    7.13  lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
    7.14    by (induct l) (simp_all add: ac_simps)
    7.15  
    7.16 +lemma subseteq_le_multiset: "A #<=# A + B"
    7.17 +unfolding le_multiset_def apply (cases B; simp)
    7.18 +apply (rule HOL.disjI1)
    7.19 +apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
    7.20 +apply (simp add: less_multiset\<^sub>H\<^sub>O)
    7.21 +done
    7.22 +
    7.23  lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
    7.24  apply (rule monoI)
    7.25  apply (unfold prefix_def)
    7.26 -apply (erule genPrefix.induct, auto)
    7.27 +apply (erule genPrefix.induct, simp_all add: add_right_mono)
    7.28  apply (erule order_trans)
    7.29 -apply simp
    7.30 +apply (simp add: less_eq_multiset_def subseteq_le_multiset)
    7.31  done
    7.32  
    7.33  (** setsum **)
     8.1 --- a/src/HOL/UNITY/Follows.thy	Mon Jun 08 22:04:19 2015 +0200
     8.2 +++ b/src/HOL/UNITY/Follows.thy	Wed Jun 10 13:24:16 2015 +0200
     8.3 @@ -168,6 +168,19 @@
     8.4  
     8.5  
     8.6  subsection{*Multiset union properties (with the multiset ordering)*}
     8.7 +(*TODO: remove when multiset is of sort ord again*)
     8.8 +instantiation multiset :: (order) ordered_ab_semigroup_add
     8.9 +begin
    8.10 +
    8.11 +definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    8.12 +  "M' < M \<longleftrightarrow> M' #<# M"
    8.13 +
    8.14 +definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    8.15 +   "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #<=# M"
    8.16 +
    8.17 +instance
    8.18 +  by default (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
    8.19 +end
    8.20  
    8.21  lemma increasing_union: 
    8.22      "[| F \<in> increasing f;  F \<in> increasing g |]