# HG changeset patch
# User blanchet
# Date 1427302294 -3600
# Node ID 6320064f22bba3026c4198a72730b7b1914f540f
# Parent  675d0c692c41f8ea8b6b759638cb995f92f8387b
more multiset theorems

diff -r 675d0c692c41 -r 6320064f22bb CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Mar 25 14:39:40 2015 +0100
+++ b/CONTRIBUTORS	Wed Mar 25 17:51:34 2015 +0100
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII, and Dmitriy Traytel, TUM
+  More multiset theorems, syntax, and operations.
+
 * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM and Jeremy Avigad, Luke Serafin, CMU
   Various integration theorems: mostly integration on intervals and substitution.
 
diff -r 675d0c692c41 -r 6320064f22bb NEWS
--- a/NEWS	Wed Mar 25 14:39:40 2015 +0100
+++ b/NEWS	Wed Mar 25 17:51:34 2015 +0100
@@ -262,6 +262,24 @@
 The "sos_cert" functionality is invoked as "sos" with additional
 argument. Minor INCOMPATIBILITY.
 
+* Theory "Library/Multiset":
+  - Introduced "replicate_mset" operation.
+  - Introduced alternative characterizations of the multiset ordering in
+    "Library/Multiset_Order".
+  - Renamed
+      in_multiset_of ~> in_multiset_in_set
+    INCOMPATIBILITY.
+  - Added attributes:
+      image_mset.id [simp]
+      image_mset_id [simp]
+      elem_multiset_of_set [simp, intro]
+      comp_fun_commute_plus_mset [simp]
+      comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]
+      in_mset_fold_plus_iff [iff]
+      set_of_Union_mset [simp]
+      in_Union_mset_iff [iff]
+    INCOMPATIBILITY.
+
 * HOL-Decision_Procs:
   - New counterexample generator quickcheck[approximation] for
     inequalities of transcendental functions.
diff -r 675d0c692c41 -r 6320064f22bb src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Mar 25 14:39:40 2015 +0100
+++ b/src/HOL/Library/Library.thy	Wed Mar 25 17:51:34 2015 +0100
@@ -42,7 +42,7 @@
   Mapping
   Monad_Syntax
   More_List
-  Multiset
+  Multiset_Order
   Numeral_Type
   NthRoot_Limits
   OptionalSugar
diff -r 675d0c692c41 -r 6320064f22bb src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Mar 25 14:39:40 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 25 17:51:34 2015 +0100
@@ -1,6 +1,9 @@
 (*  Title:      HOL/Library/Multiset.thy
     Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
     Author:     Andrei Popescu, TU Muenchen
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Mathias Fleury, MPII
 *)
 
 section {* (Finite) multisets *}
@@ -382,8 +385,7 @@
 lemma multi_psub_self[simp]: "(A::'a multiset) < A = False"
   by simp
 
-lemma mset_less_add_bothsides:
-  "T + {#x#} < S + {#x#} \<Longrightarrow> T < S"
+lemma mset_less_add_bothsides: "N + {#x#} < M + {#x#} \<Longrightarrow> N < M"
   by (fact add_less_imp_less_right)
 
 lemma mset_less_empty_nonempty:
@@ -593,6 +595,10 @@
 lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
   by (metis mset_leD subsetI mem_set_of_iff)
 
+lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
+  by auto
+
+
 subsubsection {* Size *}
 
 definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
@@ -895,12 +901,24 @@
 translations
   "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
 
+syntax (xsymbols)
+  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+      ("({#_/. _ \<in># _#})")
+translations
+  "{#e. x \<in># M#}" == "CONST image_mset (\<lambda>x. e) M"
+
 syntax
-  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+  "_comprehension3_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
       ("({#_/ | _ :# _./ _#})")
 translations
   "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
 
+syntax
+  "_comprehension4_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+      ("({#_/ | _ \<in># _./ _#})")
+translations
+  "{#e | x\<in>#M. P#}" => "{#e. x \<in># {# x\<in>#M. P#}#}"
+
 text {*
   This allows to write not just filters like @{term "{#x:#M. x<c#}"}
   but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
@@ -908,6 +926,9 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
+lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M"
+  by (metis mem_set_of_iff set_of_image_mset)
+
 functor image_mset: image_mset
 proof -
   fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
@@ -924,7 +945,19 @@
   qed
 qed
 
-declare image_mset.identity [simp]
+declare
+  image_mset.id [simp]
+  image_mset.identity [simp]
+
+lemma image_mset_id[simp]: "image_mset id x = x"
+  unfolding id_def by auto
+
+lemma image_mset_cong: "(\<And>x. x \<in># M \<Longrightarrow> f x = g x) \<Longrightarrow> {#f x. x \<in># M#} = {#g x. x \<in># M#}"
+  by (induct M) auto
+
+lemma image_mset_cong_pair:
+  "(\<forall>x y. (x, y) \<in># M \<longrightarrow> f x y = g x y) \<Longrightarrow> {#f x y. (x, y) \<in># M#} = {#g x y. (x, y) \<in># M#}"
+  by (metis image_mset_cong split_cong)
 
 
 subsection {* Further conversions *}
@@ -942,7 +975,7 @@
   by (induct xs) simp_all
 
 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
-by (induct x) auto
+  by (induct x) auto
 
 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
 by (induct x) auto
@@ -1059,10 +1092,6 @@
   "multiset_of (insort x xs) = multiset_of xs + {#x#}"
   by (induct xs) (simp_all add: ac_simps)
 
-lemma in_multiset_of:
-  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
-  by (induct xs) simp_all
-
 lemma multiset_of_map:
   "multiset_of (map f xs) = image_mset f (multiset_of xs)"
   by (induct xs) simp_all
@@ -1098,6 +1127,9 @@
   by (auto elim!: Set.set_insert)
 qed -- {* TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset} *}
 
+lemma elem_multiset_of_set[simp, intro]: "finite A \<Longrightarrow> x \<in># multiset_of_set A \<longleftrightarrow> x \<in> A"
+  by (induct A rule: finite_induct) simp_all
+
 context linorder
 begin
 
@@ -1186,6 +1218,14 @@
 
 end
 
+lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + \<Colon> 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
+  by default (simp add: add_ac comp_def)
+
+declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
+
+lemma in_mset_fold_plus_iff[iff]: "x \<in># Multiset.fold (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
+  by (induct NN) auto
+
 notation times (infixl "*" 70)
 notation Groups.one ("1")
 
@@ -1210,6 +1250,22 @@
 
 end
 
+lemma msetsum_diff:
+  fixes M N :: "('a \<Colon> ordered_cancel_comm_monoid_diff) multiset"
+  shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
+  by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
+
+abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
+  "Union_mset MM \<equiv> msetsum MM"
+
+notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
+
+lemma set_of_Union_mset[simp]: "set_of (\<Union># MM) = (\<Union>M \<in> set_of MM. set_of M)"
+  by (induct MM) auto
+
+lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
+  by (induct MM) auto
+
 syntax
   "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
       ("(3SUM _:#_. _)" [0, 51, 10] 10)
@@ -1338,6 +1394,46 @@
 lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
   by (rule mcard_mono[OF multiset_filter_subset])
 
+lemma mcard_1_singleton:
+  assumes card: "mcard AA = 1"
+  shows "\<exists>A. AA = {#A#}"
+  using card by (cases AA) auto
+
+lemma mcard_Diff_subset:
+  assumes "M \<le> M'"
+  shows "mcard (M' - M) = mcard M' - mcard M"
+  by (metis add_diff_cancel_left' assms mcard_plus mset_le_exists_conv)
+
+
+subsection {* Replicate operation *}
+
+definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
+  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
+
+lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
+  unfolding replicate_mset_def by simp
+
+lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
+  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
+
+lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
+  unfolding replicate_mset_def by (induct n) simp_all
+
+lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
+  unfolding replicate_mset_def by (induct n) simp_all
+
+lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
+  by (auto split: if_splits)
+
+lemma mcard_replicate_mset[simp]: "mcard (replicate_mset n M) = n"
+  by (induct n, simp_all)
+
+lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le> M"
+  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset less_eq_multiset.rep_eq)
+
+lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
+  by (induct D) simp_all
+
 
 subsection {* Alternative representations *}
 
@@ -1790,7 +1886,7 @@
 qed (auto simp add: le_multiset_def intro: union_less_mono2)
 
 
-subsection {* Termination proofs with multiset orders *}
+subsubsection {* Termination proofs with multiset orders *}
 
 lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
   and multi_member_this: "x \<in># {# x #} + XS"
@@ -2082,9 +2178,7 @@
   then show ?thesis by simp
 qed
 
-lemma [code_unfold]:
-  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
-  by (simp add: in_multiset_of)
+declare in_multiset_in_set [code_unfold]
 
 lemma [code]:
   "count (multiset_of xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
@@ -2094,25 +2188,19 @@
   then show ?thesis by simp
 qed
 
-lemma [code]:
-  "set_of (multiset_of xs) = set xs"
-  by simp
-
-lemma [code]:
-  "sorted_list_of_multiset (multiset_of xs) = sort xs"
-  by (induct xs) simp_all
+declare set_of_multiset_of [code]
+
+declare sorted_list_of_multiset_multiset_of [code]
 
 lemma [code]: -- {* not very efficient, but representation-ignorant! *}
   "multiset_of_set A = multiset_of (sorted_list_of_set A)"
   apply (cases "finite A")
   apply simp_all
   apply (induct A rule: finite_induct)
-  apply (simp_all add: union_commute)
+  apply (simp_all add: add.commute)
   done
 
-lemma [code]:
-  "mcard (multiset_of xs) = length xs"
-  by (simp add: mcard_multiset_of)
+declare mcard_multiset_of [code]
 
 fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
@@ -2287,7 +2375,7 @@
   have "multiset_of xs' = {#x#} + multiset_of xsa"
     unfolding xsa_def using j_len nth_j
     by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
-      multiset_of.simps(2) union_code union_commute)
+      multiset_of.simps(2) union_code add.commute)
   hence ms_x: "multiset_of xsa = multiset_of xs"
     by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
   then obtain ysa where
@@ -2344,7 +2432,7 @@
     by (rule image_mset.id)
 next
   show "\<And>f g. image_mset (g \<circ> f) = image_mset g \<circ> image_mset f"
-    unfolding comp_def by (rule ext) (simp add: image_mset.compositionality comp_def)
+    unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
 next
   fix X :: "'a multiset"
   show "\<And>f g. (\<And>z. z \<in> set_of X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X"
diff -r 675d0c692c41 -r 6320064f22bb src/HOL/Library/Multiset_Order.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Mar 25 17:51:34 2015 +0100
@@ -0,0 +1,308 @@
+(*  Title:      HOL/Library/Multiset_Order.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+*)
+
+section {* More Theorems about the Multiset Order *}
+
+theory Multiset_Order
+imports Multiset
+begin
+
+subsubsection {* Alternative characterizations *}
+
+context order
+begin
+
+lemma reflp_le: "reflp (op \<le>)"
+  unfolding reflp_def by simp
+
+lemma antisymP_le: "antisymP (op \<le>)"
+  unfolding antisym_def by auto
+
+lemma transp_le: "transp (op \<le>)"
+  unfolding transp_def by auto
+
+lemma irreflp_less: "irreflp (op <)"
+  unfolding irreflp_def by simp
+
+lemma antisymP_less: "antisymP (op <)"
+  unfolding antisym_def by auto
+
+lemma transp_less: "transp (op <)"
+  unfolding transp_def by auto
+
+lemmas le_trans = transp_le[unfolded transp_def, rule_format]
+
+lemma order_mult: "class.order
+  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
+  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
+  (is "class.order ?le ?less")
+proof -
+  have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M"
+  proof
+    fix M :: "'a multiset"
+    have "trans {(x'::'a, x). x' < x}"
+      by (rule transI) simp
+    moreover
+    assume "(M, M) \<in> mult {(x, y). x < y}"
+    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
+      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
+      by (rule mult_implies_one_step)
+    then obtain I J K where "M = I + J" and "M = I + K"
+      and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
+    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
+    have "finite (set_of K)" by simp
+    moreover note aux2
+    ultimately have "set_of K = {}"
+      by (induct rule: finite_induct)
+       (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
+    with aux1 show False by simp
+  qed
+  have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
+    unfolding mult_def by (blast intro: trancl_trans)
+  show "class.order ?le ?less"
+    by default (auto simp add: le_multiset_def irrefl dest: trans)
+qed
+
+text {* The Dershowitz--Manna ordering: *}
+
+definition less_multiset\<^sub>D\<^sub>M where
+  "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
+   (\<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)))"
+
+
+text {* The Huet--Oppen ordering: *}
+
+definition less_multiset\<^sub>H\<^sub>O where
+  "less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
+
+lemma mult_imp_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+proof (unfold mult_def less_multiset\<^sub>H\<^sub>O_def, induct rule: trancl_induct)
+  case (base P)
+  then show ?case unfolding mult1_def by force
+next
+  case (step N P)
+  from step(2) obtain M0 a K where
+    *: "P = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
+    unfolding mult1_def by blast
+  then have count_K_a: "count K a = 0" by auto
+  with step(3) *(1,2) have "M \<noteq> P" by (force dest: *(3) split: if_splits)
+  moreover
+  { assume "count P a \<le> count M a"
+    with count_K_a have "count N a < count M a" unfolding *(1,2) by auto
+      with step(3) obtain z where z: "z > a" "count M z < count N z" by blast
+      with * have "count N z \<le> count P z" by force
+      with z have "\<exists>z > a. count M z < count P z" by auto
+  } note count_a = this
+  { fix y
+    assume count_y: "count P y < count M y"
+    have "\<exists>x>y. count M x < count P x"
+    proof (cases "y = a")
+      case True
+      with count_y count_a show ?thesis by auto
+    next
+      case False
+      show ?thesis
+      proof (cases "y \<in># K")
+        case True
+        with *(3) have "y < a" by simp
+        then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
+      next
+        case False
+        with `y \<noteq> a` have "count P y = count N y" unfolding *(1,2) by simp
+        with count_y step(3) obtain z where z: "z > y" "count M z < count N z" by auto
+        show ?thesis
+        proof (cases "z \<in># K")
+          case True
+          with *(3) have "z < a" by simp
+          with z(1) show ?thesis
+            by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
+        next
+          case False
+          with count_K_a have "count N z \<le> count P z" unfolding * by auto
+          with z show ?thesis by auto
+        qed
+      qed
+    qed
+  }
+  ultimately show ?case by blast
+qed
+
+lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
+  "less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}"
+proof -
+  assume "less_multiset\<^sub>D\<^sub>M M N"
+  then obtain X Y where
+    "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)"
+    unfolding less_multiset\<^sub>D\<^sub>M_def by blast
+  then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
+    by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
+  with `M = N - X + Y` `X \<le> N` show "(M, N) \<in> mult {(x, y). x < y}"
+    by (metis ordered_cancel_comm_monoid_diff_class.diff_add)
+qed
+
+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"
+unfolding less_multiset\<^sub>D\<^sub>M_def
+proof (intro iffI exI conjI)
+  assume "less_multiset\<^sub>H\<^sub>O M N"
+  then obtain z where z: "count M z < count N z"
+    unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff)
+  def X \<equiv> "N - M"
+  def Y \<equiv> "M - N"
+  from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
+  from z show "X \<le> N" unfolding X_def by auto
+  show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
+  show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
+  proof (intro allI impI)
+    fix k
+    assume "k \<in># Y"
+    then have "count N k < count M k" unfolding Y_def by auto
+    with `less_multiset\<^sub>H\<^sub>O M N` obtain a where "k < a" and "count M a < count N a"
+      unfolding less_multiset\<^sub>H\<^sub>O_def by blast
+    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def by auto
+  qed
+qed
+
+lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N"
+  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+
+lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+  by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O)
+
+lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def]
+lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def]
+
+end
+
+context linorder
+begin
+
+lemma total_le: "total {(a \<Colon> 'a, b). a \<le> b}"
+  unfolding total_on_def by auto
+
+lemma total_less: "total {(a \<Colon> 'a, b). a < b}"
+  unfolding total_on_def by auto
+
+lemma linorder_mult: "class.linorder
+  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)
+  (\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
+proof -
+  interpret o: order
+    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)"
+    "(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})"
+    by (rule order_mult)
+  show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
+qed
+
+end
+
+lemma less_multiset_less_multiset\<^sub>H\<^sub>O:
+  "M \<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+  unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
+
+lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
+lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
+
+lemma le_multiset\<^sub>H\<^sub>O:
+  fixes M N :: "('a \<Colon> linorder) multiset"
+  shows "M \<subseteq># N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
+  by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
+
+lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M \<subset># N}"
+  unfolding less_multiset_def by (auto intro: wf_mult wf)
+
+lemma order_multiset: "class.order
+  (le_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)
+  (less_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)"
+  by unfold_locales
+
+lemma linorder_multiset: "class.linorder
+  (le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)
+  (less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)"
+  by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq)
+
+interpretation multiset_linorder: linorder
+  "le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
+  "less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool"
+  by (rule linorder_multiset)
+
+interpretation multiset_wellorder: wellorder
+  "le_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
+  "less_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool"
+  by unfold_locales (blast intro: wf_less_multiset[unfolded wf_def, rule_format])
+
+lemma le_multiset_total:
+  fixes M N :: "('a \<Colon> linorder) multiset"
+  shows "\<not> M \<subseteq># N \<Longrightarrow> N \<subseteq># M"
+  by (metis multiset_linorder.le_cases)
+
+lemma less_eq_imp_le_multiset:
+  fixes M N :: "('a \<Colon> linorder) multiset"
+  shows "M \<le> N \<Longrightarrow> M \<subseteq># N"
+  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
+  by (auto dest: leD simp add: less_eq_multiset.rep_eq)
+
+lemma less_multiset_right_total:
+  fixes M :: "('a \<Colon> linorder) multiset"
+  shows "M \<subset># M + {#undefined#}"
+  unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+
+lemma le_multiset_empty_left[simp]:
+  fixes M :: "('a \<Colon> linorder) multiset"
+  shows "{#} \<subseteq># M"
+  by (simp add: less_eq_imp_le_multiset)
+
+lemma le_multiset_empty_right[simp]:
+  fixes M :: "('a \<Colon> linorder) multiset"
+  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<subseteq># {#}"
+  by (metis le_multiset_empty_left multiset_order.antisym)
+
+lemma less_multiset_empty_left[simp]:
+  fixes M :: "('a \<Colon> linorder) multiset"
+  shows "M \<noteq> {#} \<Longrightarrow> {#} \<subset># M"
+  by (simp add: less_multiset\<^sub>H\<^sub>O)
+
+lemma less_multiset_empty_right[simp]:
+  fixes M :: "('a \<Colon> linorder) multiset"
+  shows "\<not> M \<subset># {#}"
+  using le_empty less_multiset\<^sub>D\<^sub>M by blast
+
+lemma
+  fixes M N :: "('a \<Colon> linorder) multiset"
+  shows
+    le_multiset_plus_left[simp]: "N \<subseteq># (M + N)" and
+    le_multiset_plus_right[simp]: "M \<subseteq># (M + N)"
+  using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+
+
+lemma
+  fixes M N :: "('a \<Colon> linorder) multiset"
+  shows
+    less_multiset_plus_plus_left_iff[simp]: "M + N \<subset># M' + N \<longleftrightarrow> M \<subset># M'" and
+    less_multiset_plus_plus_right_iff[simp]: "M + N \<subset># M + N' \<longleftrightarrow> N \<subset># N'"
+  unfolding less_multiset\<^sub>H\<^sub>O by auto
+
+lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
+  by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral)
+
+lemma
+  fixes M N :: "('a \<Colon> linorder) multiset"
+  shows
+    less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N \<subset># M + N" and
+    less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M \<subset># M + N"
+  using [[metis_verbose = false]]
+  by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff
+    add.commute)+
+
+lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M \<subset># N"
+  unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
+
+lemma ex_gt_count_imp_less_multiset:
+  "(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M \<subset># N"
+  unfolding less_multiset\<^sub>H\<^sub>O by (metis UnCI comm_monoid_diff_class.diff_cancel dual_order.asym
+    less_imp_diff_less mem_set_of_iff order.not_eq_order_implies_strict set_of_union)
+
+lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N \<subset># P \<Longrightarrow> M - P + N \<subset># M"
+  by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
+
+end