--- 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.
--- 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.
--- 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
--- 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"
--- /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