src/HOL/Library/Multiset.thy

added lemma image_mset_filter_mset_swap

(*  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
    Author:     Martin Desharnais, MPI-INF Saarbruecken
*)

section \<open>(Finite) Multisets\<close>

theory Multiset
  imports Cancellation
begin

subsection \<open>The type of multisets\<close>

typedef 'a multiset = \<open>{f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}\<close>
  morphisms count Abs_multiset
proof
  show \<open>(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}\<close>
    by simp
qed

setup_lifting type_definition_multiset

lemma count_Abs_multiset:
  \<open>count (Abs_multiset f) = f\<close> if \<open>finite {x. f x > 0}\<close>
  by (rule Abs_multiset_inverse) (simp add: that)

lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
  by (simp only: count_inject [symmetric] fun_eq_iff)

lemma multiset_eqI: "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
  using multiset_eq_iff by auto

text \<open>Preservation of the representing set \<^term>\<open>multiset\<close>.\<close>

lemma diff_preserves_multiset:
  \<open>finite {x. 0 < M x - N x}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
  using that by (rule rev_finite_subset) auto

lemma filter_preserves_multiset:
  \<open>finite {x. 0 < (if P x then M x else 0)}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
  using that by (rule rev_finite_subset) auto

lemmas in_multiset = diff_preserves_multiset filter_preserves_multiset


subsection \<open>Representing multisets\<close>

text \<open>Multiset enumeration\<close>

instantiation multiset :: (type) cancel_comm_monoid_add
begin

lift_definition zero_multiset :: \<open>'a multiset\<close>
  is \<open>\<lambda>a. 0\<close>
  by simp

abbreviation empty_mset :: \<open>'a multiset\<close> (\<open>{#}\<close>)
  where \<open>empty_mset \<equiv> 0\<close>

lift_definition plus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
  is \<open>\<lambda>M N a. M a + N a\<close>
  by simp

lift_definition minus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
  is \<open>\<lambda>M N a. M a - N a\<close>
  by (rule diff_preserves_multiset)

instance
  by (standard; transfer) (simp_all add: fun_eq_iff)

end

context
begin

qualified definition is_empty :: "'a multiset \<Rightarrow> bool" where
  [code_abbrev]: "is_empty A \<longleftrightarrow> A = {#}"

end

lemma add_mset_in_multiset:
  \<open>finite {x. 0 < (if x = a then Suc (M x) else M x)}\<close>
  if \<open>finite {x. 0 < M x}\<close>
  using that by (simp add: flip: insert_Collect)

lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
  "\<lambda>a M b. if b = a then Suc (M b) else M b"
by (rule add_mset_in_multiset)

syntax
  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
translations
  "{#x, xs#}" == "CONST add_mset x {#xs#}"
  "{#x#}" == "CONST add_mset x {#}"

lemma count_empty [simp]: "count {#} a = 0"
  by (simp add: zero_multiset.rep_eq)

lemma count_add_mset [simp]:
  "count (add_mset b A) a = (if b = a then Suc (count A a) else count A a)"
  by (simp add: add_mset.rep_eq)

lemma count_single: "count {#b#} a = (if b = a then 1 else 0)"
  by simp

lemma
  add_mset_not_empty [simp]: \<open>add_mset a A \<noteq> {#}\<close> and
  empty_not_add_mset [simp]: "{#} \<noteq> add_mset a A"
  by (auto simp: multiset_eq_iff)

lemma add_mset_add_mset_same_iff [simp]:
  "add_mset a A = add_mset a B \<longleftrightarrow> A = B"
  by (auto simp: multiset_eq_iff)

lemma add_mset_commute:
  "add_mset x (add_mset y M) = add_mset y (add_mset x M)"
  by (auto simp: multiset_eq_iff)


subsection \<open>Basic operations\<close>

subsubsection \<open>Conversion to set and membership\<close>

definition set_mset :: \<open>'a multiset \<Rightarrow> 'a set\<close>
  where \<open>set_mset M = {x. count M x > 0}\<close>

abbreviation member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
  where \<open>member_mset a M \<equiv> a \<in> set_mset M\<close>

notation
  member_mset  (\<open>'(\<in>#')\<close>) and
  member_mset  (\<open>(_/ \<in># _)\<close> [50, 51] 50)

notation  (ASCII)
  member_mset  (\<open>'(:#')\<close>) and
  member_mset  (\<open>(_/ :# _)\<close> [50, 51] 50)

abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
  where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close>

notation
  not_member_mset  (\<open>'(\<notin>#')\<close>) and
  not_member_mset  (\<open>(_/ \<notin># _)\<close> [50, 51] 50)

notation  (ASCII)
  not_member_mset  (\<open>'(~:#')\<close>) and
  not_member_mset  (\<open>(_/ ~:# _)\<close> [50, 51] 50)

context
begin

qualified abbreviation Ball :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
  where "Ball M \<equiv> Set.Ball (set_mset M)"

qualified abbreviation Bex :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
  where "Bex M \<equiv> Set.Bex (set_mset M)"

end

syntax
  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10)
  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10)

syntax  (ASCII)
  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_:#_./ _)" [0, 0, 10] 10)
  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_:#_./ _)" [0, 0, 10] 10)

translations
  "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
  "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"

print_translation \<open>
 [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Ball\<close> \<^syntax_const>\<open>_MBall\<close>,
  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Bex\<close> \<^syntax_const>\<open>_MBex\<close>]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>

lemma count_eq_zero_iff:
  "count M x = 0 \<longleftrightarrow> x \<notin># M"
  by (auto simp add: set_mset_def)

lemma not_in_iff:
  "x \<notin># M \<longleftrightarrow> count M x = 0"
  by (auto simp add: count_eq_zero_iff)

lemma count_greater_zero_iff [simp]:
  "count M x > 0 \<longleftrightarrow> x \<in># M"
  by (auto simp add: set_mset_def)

lemma count_inI:
  assumes "count M x = 0 \<Longrightarrow> False"
  shows "x \<in># M"
proof (rule ccontr)
  assume "x \<notin># M"
  with assms show False by (simp add: not_in_iff)
qed

lemma in_countE:
  assumes "x \<in># M"
  obtains n where "count M x = Suc n"
proof -
  from assms have "count M x > 0" by simp
  then obtain n where "count M x = Suc n"
    using gr0_conv_Suc by blast
  with that show thesis .
qed

lemma count_greater_eq_Suc_zero_iff [simp]:
  "count M x \<ge> Suc 0 \<longleftrightarrow> x \<in># M"
  by (simp add: Suc_le_eq)

lemma count_greater_eq_one_iff [simp]:
  "count M x \<ge> 1 \<longleftrightarrow> x \<in># M"
  by simp

lemma set_mset_empty [simp]:
  "set_mset {#} = {}"
  by (simp add: set_mset_def)

lemma set_mset_single:
  "set_mset {#b#} = {b}"
  by (simp add: set_mset_def)

lemma set_mset_eq_empty_iff [simp]:
  "set_mset M = {} \<longleftrightarrow> M = {#}"
  by (auto simp add: multiset_eq_iff count_eq_zero_iff)

lemma finite_set_mset [iff]:
  "finite (set_mset M)"
  using count [of M] by simp

lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
  by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits)

lemma multiset_nonemptyE [elim]:
  assumes "A \<noteq> {#}"
  obtains x where "x \<in># A"
proof -
  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
  with that show ?thesis by blast
qed


subsubsection \<open>Union\<close>

lemma count_union [simp]:
  "count (M + N) a = count M a + count N a"
  by (simp add: plus_multiset.rep_eq)

lemma set_mset_union [simp]:
  "set_mset (M + N) = set_mset M \<union> set_mset N"
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_union) simp

lemma union_mset_add_mset_left [simp]:
  "add_mset a A + B = add_mset a (A + B)"
  by (auto simp: multiset_eq_iff)

lemma union_mset_add_mset_right [simp]:
  "A + add_mset a B = add_mset a (A + B)"
  by (auto simp: multiset_eq_iff)

lemma add_mset_add_single: \<open>add_mset a A = A + {#a#}\<close>
  by (subst union_mset_add_mset_right, subst add.comm_neutral) standard


subsubsection \<open>Difference\<close>

instance multiset :: (type) comm_monoid_diff
  by standard (transfer; simp add: fun_eq_iff)

lemma count_diff [simp]:
  "count (M - N) a = count M a - count N a"
  by (simp add: minus_multiset.rep_eq)

lemma add_mset_diff_bothsides:
  \<open>add_mset a M - add_mset a A = M - A\<close>
  by (auto simp: multiset_eq_iff)

lemma in_diff_count:
  "a \<in># M - N \<longleftrightarrow> count N a < count M a"
  by (simp add: set_mset_def)

lemma count_in_diffI:
  assumes "\<And>n. count N x = n + count M x \<Longrightarrow> False"
  shows "x \<in># M - N"
proof (rule ccontr)
  assume "x \<notin># M - N"
  then have "count N x = (count N x - count M x) + count M x"
    by (simp add: in_diff_count not_less)
  with assms show False by auto
qed

lemma in_diff_countE:
  assumes "x \<in># M - N"
  obtains n where "count M x = Suc n + count N x"
proof -
  from assms have "count M x - count N x > 0" by (simp add: in_diff_count)
  then have "count M x > count N x" by simp
  then obtain n where "count M x = Suc n + count N x"
    using less_iff_Suc_add by auto
  with that show thesis .
qed

lemma in_diffD:
  assumes "a \<in># M - N"
  shows "a \<in># M"
proof -
  have "0 \<le> count N a" by simp
  also from assms have "count N a < count M a"
    by (simp add: in_diff_count)
  finally show ?thesis by simp
qed

lemma set_mset_diff:
  "set_mset (M - N) = {a. count N a < count M a}"
  by (simp add: set_mset_def)

lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
  by rule (fact Groups.diff_zero, fact Groups.zero_diff)

lemma diff_cancel: "A - A = {#}"
  by (fact Groups.diff_cancel)

lemma diff_union_cancelR: "M + N - N = (M::'a multiset)"
  by (fact add_diff_cancel_right')

lemma diff_union_cancelL: "N + M - N = (M::'a multiset)"
  by (fact add_diff_cancel_left')

lemma diff_right_commute:
  fixes M N Q :: "'a multiset"
  shows "M - N - Q = M - Q - N"
  by (fact diff_right_commute)

lemma diff_add:
  fixes M N Q :: "'a multiset"
  shows "M - (N + Q) = M - N - Q"
  by (rule sym) (fact diff_diff_add)

lemma insert_DiffM [simp]: "x \<in># M \<Longrightarrow> add_mset x (M - {#x#}) = M"
  by (clarsimp simp: multiset_eq_iff)

lemma insert_DiffM2: "x \<in># M \<Longrightarrow> (M - {#x#}) + {#x#} = M"
  by simp

lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> add_mset b (M - {#a#}) = add_mset b M - {#a#}"
  by (auto simp add: multiset_eq_iff)

lemma diff_add_mset_swap [simp]: "b \<notin># A \<Longrightarrow> add_mset b M - A = add_mset b (M - A)"
  by (auto simp add: multiset_eq_iff simp: not_in_iff)

lemma diff_union_swap2 [simp]: "y \<in># M \<Longrightarrow> add_mset x M - {#y#} = add_mset x (M - {#y#})"
  by (metis add_mset_diff_bothsides diff_union_swap diff_zero insert_DiffM)

lemma diff_diff_add_mset [simp]: "(M::'a multiset) - N - P = M - (N + P)"
  by (rule diff_diff_add)

lemma diff_union_single_conv:
  "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
  by (simp add: multiset_eq_iff Suc_le_eq)

lemma mset_add [elim?]:
  assumes "a \<in># A"
  obtains B where "A = add_mset a B"
proof -
  from assms have "A = add_mset a (A - {#a#})"
    by simp
  with that show thesis .
qed

lemma union_iff:
  "a \<in># A + B \<longleftrightarrow> a \<in># A \<or> a \<in># B"
  by auto


subsubsection \<open>Min and Max\<close>

abbreviation Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
"Min_mset m \<equiv> Min (set_mset m)"

abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
"Max_mset m \<equiv> Max (set_mset m)"


subsubsection \<open>Equality of multisets\<close>

lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
  by (auto simp add: multiset_eq_iff)

lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
  by (auto simp add: multiset_eq_iff)

lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
  by (auto simp add: multiset_eq_iff)

lemma multi_self_add_other_not_self [simp]: "M = add_mset x M \<longleftrightarrow> False"
  by (auto simp add: multiset_eq_iff)

lemma add_mset_remove_trivial [simp]: \<open>add_mset x M - {#x#} = M\<close>
  by (auto simp: multiset_eq_iff)

lemma diff_single_trivial: "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
  by (auto simp add: multiset_eq_iff not_in_iff)

lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = add_mset x N"
  by auto

lemma union_single_eq_diff: "add_mset x M = N \<Longrightarrow> M = N - {#x#}"
  unfolding add_mset_add_single[of _ M] by (fact add_implies_diff)

lemma union_single_eq_member: "add_mset x M = N \<Longrightarrow> x \<in># N"
  by auto

lemma add_mset_remove_trivial_If:
  "add_mset a (N - {#a#}) = (if a \<in># N then N else add_mset a N)"
  by (simp add: diff_single_trivial)

lemma add_mset_remove_trivial_eq: \<open>N = add_mset a (N - {#a#}) \<longleftrightarrow> a \<in># N\<close>
  by (auto simp: add_mset_remove_trivial_If)

lemma union_is_single:
  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
  (is "?lhs = ?rhs")
proof
  show ?lhs if ?rhs using that by auto
  show ?rhs if ?lhs
    by (metis Multiset.diff_cancel add.commute add_diff_cancel_left' diff_add_zero diff_single_trivial insert_DiffM that)
qed

lemma single_is_union: "{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N"
  by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single)

lemma add_eq_conv_diff:
  "add_mset a M = add_mset b N \<longleftrightarrow> M = N \<and> a = b \<or> M = add_mset b (N - {#a#}) \<and> N = add_mset a (M - {#b#})"
  (is "?lhs \<longleftrightarrow> ?rhs")
(* shorter: by (simp add: multiset_eq_iff) fastforce *)
proof
  show ?lhs if ?rhs
    using that
    by (auto simp add: add_mset_commute[of a b])
  show ?rhs if ?lhs
  proof (cases "a = b")
    case True with \<open>?lhs\<close> show ?thesis by simp
  next
    case False
    from \<open>?lhs\<close> have "a \<in># add_mset b N" by (rule union_single_eq_member)
    with False have "a \<in># N" by auto
    moreover from \<open>?lhs\<close> have "M = add_mset b N - {#a#}" by (rule union_single_eq_diff)
    moreover note False
    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"])
  qed
qed

lemma add_mset_eq_single [iff]: "add_mset b M = {#a#} \<longleftrightarrow> b = a \<and> M = {#}"
  by (auto simp: add_eq_conv_diff)

lemma single_eq_add_mset [iff]: "{#a#} = add_mset b M \<longleftrightarrow> b = a \<and> M = {#}"
  by (auto simp: add_eq_conv_diff)

lemma insert_noteq_member:
  assumes BC: "add_mset b B = add_mset c C"
   and bnotc: "b \<noteq> c"
  shows "c \<in># B"
proof -
  have "c \<in># add_mset c C" by simp
  have nc: "\<not> c \<in># {#b#}" using bnotc by simp
  then have "c \<in># add_mset b B" using BC by simp
  then show "c \<in># B" using nc by simp
qed

lemma add_eq_conv_ex:
  "(add_mset a M = add_mset b N) =
    (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))"
  by (auto simp add: add_eq_conv_diff)

lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = add_mset x A"
  by (rule exI [where x = "M - {#x#}"]) simp

lemma multiset_add_sub_el_shuffle:
  assumes "c \<in># B"
    and "b \<noteq> c"
  shows "add_mset b (B - {#c#}) = add_mset b B - {#c#}"
proof -
  from \<open>c \<in># B\<close> obtain A where B: "B = add_mset c A"
    by (blast dest: multi_member_split)
  have "add_mset b A = add_mset c (add_mset b A) - {#c#}" by simp
  then have "add_mset b A = add_mset b (add_mset c A) - {#c#}"
    by (simp add: \<open>b \<noteq> c\<close>)
  then show ?thesis using B by simp
qed

lemma add_mset_eq_singleton_iff[iff]:
  "add_mset x M = {#y#} \<longleftrightarrow> M = {#} \<and> x = y"
  by auto


subsubsection \<open>Pointwise ordering induced by count\<close>

definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
  where "A \<subseteq># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"

definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
  where "A \<subset># B \<longleftrightarrow> A \<subseteq># B \<and> A \<noteq> B"

abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supseteq>#" 50)
  where "supseteq_mset A B \<equiv> B \<subseteq># A"

abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supset>#" 50)
  where "supset_mset A B \<equiv> B \<subset># A"

notation (input)
  subseteq_mset  (infix "\<le>#" 50) and
  supseteq_mset  (infix "\<ge>#" 50)

notation (ASCII)
  subseteq_mset  (infix "<=#" 50) and
  subset_mset  (infix "<#" 50) and
  supseteq_mset  (infix ">=#" 50) and
  supset_mset  (infix ">#" 50)

global_interpretation subset_mset: ordering \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order.trans order.antisym)

interpretation subset_mset: ordered_ab_semigroup_add_imp_le \<open>(+)\<close> \<open>(-)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(\<subseteq>#)" "(\<subset>#)"
  by standard
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

lemma mset_subset_eqI:
  "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
  by (simp add: subseteq_mset_def)

lemma mset_subset_eq_count:
  "A \<subseteq># B \<Longrightarrow> count A a \<le> count B a"
  by (simp add: subseteq_mset_def)

lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
  unfolding subseteq_mset_def
  apply (rule iffI)
   apply (rule exI [where x = "B - A"])
   apply (auto intro: multiset_eq_iff [THEN iffD2])
  done

interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)"
  by standard (simp, fact mset_subset_eq_exists_conv)
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp]

lemma mset_subset_eq_mono_add_right_cancel: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
   by (fact subset_mset.add_le_cancel_right)

lemma mset_subset_eq_mono_add_left_cancel: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
   by (fact subset_mset.add_le_cancel_left)

lemma mset_subset_eq_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
   by (fact subset_mset.add_mono)

lemma mset_subset_eq_add_left: "(A::'a multiset) \<subseteq># A + B"
   by simp

lemma mset_subset_eq_add_right: "B \<subseteq># (A::'a multiset) + B"
   by simp

lemma single_subset_iff [simp]:
  "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
  by (auto simp add: subseteq_mset_def Suc_le_eq)

lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
  by simp

lemma mset_subset_eq_add_mset_cancel: \<open>add_mset a A \<subseteq># add_mset a B \<longleftrightarrow> A \<subseteq># B\<close>
  unfolding add_mset_add_single[of _ A] add_mset_add_single[of _ B]
  by (rule mset_subset_eq_mono_add_right_cancel)

lemma multiset_diff_union_assoc:
  fixes A B C D :: "'a multiset"
  shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)"
  by (fact subset_mset.diff_add_assoc)

lemma mset_subset_eq_multiset_union_diff_commute:
  fixes A B C D :: "'a multiset"
  shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B"
  by (fact subset_mset.add_diff_assoc2)

lemma diff_subset_eq_self[simp]:
  "(M::'a multiset) - N \<subseteq># M"
  by (simp add: subseteq_mset_def)

lemma mset_subset_eqD:
  assumes "A \<subseteq># B" and "x \<in># A"
  shows "x \<in># B"
proof -
  from \<open>x \<in># A\<close> have "count A x > 0" by simp
  also from \<open>A \<subseteq># B\<close> have "count A x \<le> count B x"
    by (simp add: subseteq_mset_def)
  finally show ?thesis by simp
qed

lemma mset_subsetD:
  "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
  by (auto intro: mset_subset_eqD [of A])

lemma set_mset_mono:
  "A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
  by (metis mset_subset_eqD subsetI)

lemma mset_subset_eq_insertD:
  "add_mset x A \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
apply (rule conjI)
 apply (simp add: mset_subset_eqD)
 apply (clarsimp simp: subset_mset_def subseteq_mset_def)
 apply safe
  apply (erule_tac x = a in allE)
  apply (auto split: if_split_asm)
done

lemma mset_subset_insertD:
  "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
  by (rule mset_subset_eq_insertD) simp

lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
  by (simp only: subset_mset.not_less_zero)

lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M"
  by (auto intro: subset_mset.gr_zeroI)

lemma empty_le: "{#} \<subseteq># A"
  by (fact subset_mset.zero_le)

lemma insert_subset_eq_iff:
  "add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
  using le_diff_conv2 [of "Suc 0" "count B a" "count A a"]
  apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq)
  apply (rule ccontr)
  apply (auto simp add: not_in_iff)
  done

lemma insert_union_subset_iff:
  "add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
  by (auto simp add: insert_subset_eq_iff subset_mset_def)

lemma subset_eq_diff_conv:
  "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
  by (simp add: subseteq_mset_def le_diff_conv)

lemma multi_psub_of_add_self [simp]: "A \<subset># add_mset x A"
  by (auto simp: subset_mset_def subseteq_mset_def)

lemma multi_psub_self: "A \<subset># A = False"
  by simp

lemma mset_subset_add_mset [simp]: "add_mset x N \<subset># add_mset x M \<longleftrightarrow> N \<subset># M"
  unfolding add_mset_add_single[of _ N] add_mset_add_single[of _ M]
  by (fact subset_mset.add_less_cancel_right)

lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
  by (auto simp: subset_mset_def elim: mset_add)

lemma Diff_eq_empty_iff_mset: "A - B = {#} \<longleftrightarrow> A \<subseteq># B"
  by (auto simp: multiset_eq_iff subseteq_mset_def)

lemma add_mset_subseteq_single_iff[iff]: "add_mset a M \<subseteq># {#b#} \<longleftrightarrow> M = {#} \<and> a = b"
proof
  assume A: "add_mset a M \<subseteq># {#b#}"
  then have \<open>a = b\<close>
    by (auto dest: mset_subset_eq_insertD)
  then show "M={#} \<and> a=b"
    using A by (simp add: mset_subset_eq_add_mset_cancel)
qed simp


subsubsection \<open>Intersection and bounded union\<close>

definition inter_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>  (infixl \<open>\<inter>#\<close> 70)
  where \<open>A \<inter># B = A - (A - B)\<close>

lemma count_inter_mset [simp]:
  \<open>count (A \<inter># B) x = min (count A x) (count B x)\<close>
  by (simp add: inter_mset_def)

(*global_interpretation subset_mset: semilattice_order \<open>(\<inter>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
  by standard (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def min_def)*)

interpretation subset_mset: semilattice_inf \<open>(\<inter>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
  by standard (simp_all add: multiset_eq_iff subseteq_mset_def)
  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

definition union_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>  (infixl \<open>\<union>#\<close> 70)
  where \<open>A \<union># B = A + (B - A)\<close>

lemma count_union_mset [simp]:
  \<open>count (A \<union># B) x = max (count A x) (count B x)\<close>
  by (simp add: union_mset_def)

global_interpretation subset_mset: semilattice_neutr_order \<open>(\<union>#)\<close> \<open>{#}\<close> \<open>(\<supseteq>#)\<close> \<open>(\<supset>#)\<close>
  apply standard
      apply (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def max_def)
   apply (auto simp add: le_antisym dest: sym)
   apply (metis nat_le_linear)+
  done

interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
proof -
  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
    by arith
  show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)"
    by standard (auto simp add: union_mset_def subseteq_mset_def)
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)"
  "(\<union>#)" "{#}"
  by standard auto
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>


subsubsection \<open>Additional intersection facts\<close>

lemma set_mset_inter [simp]:
  "set_mset (A \<inter># B) = set_mset A \<inter> set_mset B"
  by (simp only: set_mset_def) auto

lemma diff_intersect_left_idem [simp]:
  "M - M \<inter># N = M - N"
  by (simp add: multiset_eq_iff min_def)

lemma diff_intersect_right_idem [simp]:
  "M - N \<inter># M = M - N"
  by (simp add: multiset_eq_iff min_def)

lemma multiset_inter_single[simp]: "a \<noteq> b \<Longrightarrow> {#a#} \<inter># {#b#} = {#}"
  by (rule multiset_eqI) auto

lemma multiset_union_diff_commute:
  assumes "B \<inter># C = {#}"
  shows "A + B - C = A - C + B"
proof (rule multiset_eqI)
  fix x
  from assms have "min (count B x) (count C x) = 0"
    by (auto simp add: multiset_eq_iff)
  then have "count B x = 0 \<or> count C x = 0"
    unfolding min_def by (auto split: if_splits)
  then show "count (A + B - C) x = count (A - C + B) x"
    by auto
qed

lemma disjunct_not_in:
  "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q")
proof
  assume ?P
  show ?Q
  proof
    fix a
    from \<open>?P\<close> have "min (count A a) (count B a) = 0"
      by (simp add: multiset_eq_iff)
    then have "count A a = 0 \<or> count B a = 0"
      by (cases "count A a \<le> count B a") (simp_all add: min_def)
    then show "a \<notin># A \<or> a \<notin># B"
      by (simp add: not_in_iff)
  qed
next
  assume ?Q
  show ?P
  proof (rule multiset_eqI)
    fix a
    from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0"
      by (auto simp add: not_in_iff)
    then show "count (A \<inter># B) a = count {#} a"
      by auto
  qed
qed

lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}"
  by (meson disjunct_not_in union_iff)

lemma inter_mset_empty_distrib_left: "(A + B) \<inter># C = {#} \<longleftrightarrow> A \<inter># C = {#} \<and> B \<inter># C = {#}"
  by (meson disjunct_not_in union_iff)

lemma add_mset_inter_add_mset [simp]:
  "add_mset a A \<inter># add_mset a B = add_mset a (A \<inter># B)"
  by (rule multiset_eqI) simp

lemma add_mset_disjoint [simp]:
  "add_mset a A \<inter># B = {#} \<longleftrightarrow> a \<notin># B \<and> A \<inter># B = {#}"
  "{#} = add_mset a A \<inter># B \<longleftrightarrow> a \<notin># B \<and> {#} = A \<inter># B"
  by (auto simp: disjunct_not_in)

lemma disjoint_add_mset [simp]:
  "B \<inter># add_mset a A = {#} \<longleftrightarrow> a \<notin># B \<and> B \<inter># A = {#}"
  "{#} = A \<inter># add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A \<inter># B"
  by (auto simp: disjunct_not_in)

lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<inter># N = M \<inter># N"
  by (simp add: multiset_eq_iff not_in_iff)

lemma inter_add_left2: "x \<in># N \<Longrightarrow> (add_mset x M) \<inter># N = add_mset x (M \<inter># (N - {#x#}))"
  by (auto simp add: multiset_eq_iff elim: mset_add)

lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N \<inter># (add_mset x M) = N \<inter># M"
  by (simp add: multiset_eq_iff not_in_iff)

lemma inter_add_right2: "x \<in># N \<Longrightarrow> N \<inter># (add_mset x M) = add_mset x ((N - {#x#}) \<inter># M)"
  by (auto simp add: multiset_eq_iff elim: mset_add)

lemma disjunct_set_mset_diff:
  assumes "M \<inter># N = {#}"
  shows "set_mset (M - N) = set_mset M"
proof (rule set_eqI)
  fix a
  from assms have "a \<notin># M \<or> a \<notin># N"
    by (simp add: disjunct_not_in)
  then show "a \<in># M - N \<longleftrightarrow> a \<in># M"
    by (auto dest: in_diffD) (simp add: in_diff_count not_in_iff)
qed

lemma at_most_one_mset_mset_diff:
  assumes "a \<notin># M - {#a#}"
  shows "set_mset (M - {#a#}) = set_mset M - {a}"
  using assms by (auto simp add: not_in_iff in_diff_count set_eq_iff)

lemma more_than_one_mset_mset_diff:
  assumes "a \<in># M - {#a#}"
  shows "set_mset (M - {#a#}) = set_mset M"
proof (rule set_eqI)
  fix b
  have "Suc 0 < count M b \<Longrightarrow> count M b > 0" by arith
  then show "b \<in># M - {#a#} \<longleftrightarrow> b \<in># M"
    using assms by (auto simp add: in_diff_count)
qed

lemma inter_iff:
  "a \<in># A \<inter># B \<longleftrightarrow> a \<in># A \<and> a \<in># B"
  by simp

lemma inter_union_distrib_left:
  "A \<inter># B + C = (A + C) \<inter># (B + C)"
  by (simp add: multiset_eq_iff min_add_distrib_left)

lemma inter_union_distrib_right:
  "C + A \<inter># B = (C + A) \<inter># (C + B)"
  using inter_union_distrib_left [of A B C] by (simp add: ac_simps)

lemma inter_subset_eq_union:
  "A \<inter># B \<subseteq># A + B"
  by (auto simp add: subseteq_mset_def)


subsubsection \<open>Additional bounded union facts\<close>

lemma set_mset_sup [simp]:
  \<open>set_mset (A \<union># B) = set_mset A \<union> set_mset B\<close>
  by (simp only: set_mset_def) (auto simp add: less_max_iff_disj)

lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># N)"
  by (simp add: multiset_eq_iff not_in_iff)

lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># (N - {#x#}))"
  by (simp add: multiset_eq_iff)

lemma sup_union_right1 [simp]: "\<not> x \<in># N \<Longrightarrow> N \<union># (add_mset x M) = add_mset x (N \<union># M)"
  by (simp add: multiset_eq_iff not_in_iff)

lemma sup_union_right2: "x \<in># N \<Longrightarrow> N \<union># (add_mset x M) = add_mset x ((N - {#x#}) \<union># M)"
  by (simp add: multiset_eq_iff)

lemma sup_union_distrib_left:
  "A \<union># B + C = (A + C) \<union># (B + C)"
  by (simp add: multiset_eq_iff max_add_distrib_left)

lemma union_sup_distrib_right:
  "C + A \<union># B = (C + A) \<union># (C + B)"
  using sup_union_distrib_left [of A B C] by (simp add: ac_simps)

lemma union_diff_inter_eq_sup:
  "A + B - A \<inter># B = A \<union># B"
  by (auto simp add: multiset_eq_iff)

lemma union_diff_sup_eq_inter:
  "A + B - A \<union># B = A \<inter># B"
  by (auto simp add: multiset_eq_iff)

lemma add_mset_union:
  \<open>add_mset a A \<union># add_mset a B = add_mset a (A \<union># B)\<close>
  by (auto simp: multiset_eq_iff max_def)


subsection \<open>Replicate and repeat operations\<close>

definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
  "replicate_mset n x = (add_mset 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 = add_mset x (replicate_mset n x)"
  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)

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) auto

lift_definition repeat_mset :: \<open>nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
  is \<open>\<lambda>n M a. n * M a\<close> by simp

lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a"
  by transfer rule

lemma repeat_mset_0 [simp]:
  \<open>repeat_mset 0 M = {#}\<close>
  by transfer simp

lemma repeat_mset_Suc [simp]:
  \<open>repeat_mset (Suc n) M = M + repeat_mset n M\<close>
  by transfer simp

lemma repeat_mset_right [simp]: "repeat_mset a (repeat_mset b A) = repeat_mset (a * b) A"
  by (auto simp: multiset_eq_iff left_diff_distrib')

lemma left_diff_repeat_mset_distrib': \<open>repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\<close>
  by (auto simp: multiset_eq_iff left_diff_distrib')

lemma left_add_mult_distrib_mset:
  "repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k"
  by (auto simp: multiset_eq_iff add_mult_distrib)

lemma repeat_mset_distrib:
  "repeat_mset (m + n) A = repeat_mset m A + repeat_mset n A"
  by (auto simp: multiset_eq_iff Nat.add_mult_distrib)

lemma repeat_mset_distrib2[simp]:
  "repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B"
  by (auto simp: multiset_eq_iff add_mult_distrib2)

lemma repeat_mset_replicate_mset[simp]:
  "repeat_mset n {#a#} = replicate_mset n a"
  by (auto simp: multiset_eq_iff)

lemma repeat_mset_distrib_add_mset[simp]:
  "repeat_mset n (add_mset a A) = replicate_mset n a + repeat_mset n A"
  by (auto simp: multiset_eq_iff)

lemma repeat_mset_empty[simp]: "repeat_mset n {#} = {#}"
  by transfer simp


subsubsection \<open>Simprocs\<close>

lemma repeat_mset_iterate_add: \<open>repeat_mset n M = iterate_add n M\<close>
  unfolding iterate_add_def by (induction n) auto

lemma mset_subseteq_add_iff1:
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subseteq># n)"
  by (auto simp add: subseteq_mset_def nat_le_add_iff1)

lemma mset_subseteq_add_iff2:
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (m \<subseteq># repeat_mset (j-i) u + n)"
  by (auto simp add: subseteq_mset_def nat_le_add_iff2)

lemma mset_subset_add_iff1:
  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subset># n)"
  unfolding subset_mset_def repeat_mset_iterate_add
  by (simp add: iterate_add_eq_add_iff1 mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add])

lemma mset_subset_add_iff2:
  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># repeat_mset (j-i) u + n)"
  unfolding subset_mset_def repeat_mset_iterate_add
  by (simp add: iterate_add_eq_add_iff2 mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add])

ML_file \<open>multiset_simprocs.ML\<close>

lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close>
  by simp

declare repeat_mset_iterate_add[cancelation_simproc_pre]

declare iterate_add_distrib[cancelation_simproc_pre]
declare repeat_mset_iterate_add[symmetric, cancelation_simproc_post]

declare add_mset_not_empty[cancelation_simproc_eq_elim]
    empty_not_add_mset[cancelation_simproc_eq_elim]
    subset_mset.le_zero_eq[cancelation_simproc_eq_elim]
    empty_not_add_mset[cancelation_simproc_eq_elim]
    add_mset_not_empty[cancelation_simproc_eq_elim]
    subset_mset.le_zero_eq[cancelation_simproc_eq_elim]
    le_zero_eq[cancelation_simproc_eq_elim]

simproc_setup mseteq_cancel
  ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" |
   "add_mset a m = n" | "m = add_mset a n" |
   "replicate_mset p a = n" | "m = replicate_mset p a" |
   "repeat_mset p m = n" | "m = repeat_mset p m") =
  \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>

simproc_setup msetsubset_cancel
  ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
   "add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
   "replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
   "repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
  \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>

simproc_setup msetsubset_eq_cancel
  ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
   "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
   "replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
   "repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
  \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>

simproc_setup msetdiff_cancel
  ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
   "add_mset a m - n" | "m - add_mset a n" |
   "replicate_mset p r - n" | "m - replicate_mset p r" |
   "repeat_mset p m - n" | "m - repeat_mset p m") =
  \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>


subsubsection \<open>Conditionally complete lattice\<close>

instantiation multiset :: (type) Inf
begin

lift_definition Inf_multiset :: "'a multiset set \<Rightarrow> 'a multiset" is
  "\<lambda>A i. if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)"
proof -
  fix A :: "('a \<Rightarrow> nat) set"
  assume *: "\<And>f. f \<in> A \<Longrightarrow> finite {x. 0 < f x}"
  show \<open>finite {i. 0 < (if A = {} then 0 else INF f\<in>A. f i)}\<close>
  proof (cases "A = {}")
    case False
    then obtain f where "f \<in> A" by blast
    hence "{i. Inf ((\<lambda>f. f i) ` A) > 0} \<subseteq> {i. f i > 0}"
      by (auto intro: less_le_trans[OF _ cInf_lower])
    moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by simp
    ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
    with False show ?thesis by simp
  qed simp_all
qed

instance ..

end

lemma Inf_multiset_empty: "Inf {} = {#}"
  by transfer simp_all

lemma count_Inf_multiset_nonempty: "A \<noteq> {} \<Longrightarrow> count (Inf A) x = Inf ((\<lambda>X. count X x) ` A)"
  by transfer simp_all


instantiation multiset :: (type) Sup
begin

definition Sup_multiset :: "'a multiset set \<Rightarrow> 'a multiset" where
  "Sup_multiset A = (if A \<noteq> {} \<and> subset_mset.bdd_above A then
           Abs_multiset (\<lambda>i. Sup ((\<lambda>X. count X i) ` A)) else {#})"

lemma Sup_multiset_empty: "Sup {} = {#}"
  by (simp add: Sup_multiset_def)

lemma Sup_multiset_unbounded: "\<not> subset_mset.bdd_above A \<Longrightarrow> Sup A = {#}"
  by (simp add: Sup_multiset_def)

instance ..

end

lemma bdd_above_multiset_imp_bdd_above_count:
  assumes "subset_mset.bdd_above (A :: 'a multiset set)"
  shows   "bdd_above ((\<lambda>X. count X x) ` A)"
proof -
  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
    by (meson subset_mset.bdd_above.E)
  hence "count X x \<le> count Y x" if "X \<in> A" for X
    using that by (auto intro: mset_subset_eq_count)
  thus ?thesis by (intro bdd_aboveI[of _ "count Y x"]) auto
qed

lemma bdd_above_multiset_imp_finite_support:
  assumes "A \<noteq> {}" "subset_mset.bdd_above (A :: 'a multiset set)"
  shows   "finite (\<Union>X\<in>A. {x. count X x > 0})"
proof -
  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
    by (meson subset_mset.bdd_above.E)
  hence "count X x \<le> count Y x" if "X \<in> A" for X x
    using that by (auto intro: mset_subset_eq_count)
  hence "(\<Union>X\<in>A. {x. count X x > 0}) \<subseteq> {x. count Y x > 0}"
    by safe (erule less_le_trans)
  moreover have "finite \<dots>" by simp
  ultimately show ?thesis by (rule finite_subset)
qed

lemma Sup_multiset_in_multiset:
  \<open>finite {i. 0 < (SUP M\<in>A. count M i)}\<close>
  if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
proof -
  have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})"
  proof safe
    fix i assume pos: "(SUP X\<in>A. count X i) > 0"
    show "i \<in> (\<Union>X\<in>A. {i. 0 < count X i})"
    proof (rule ccontr)
      assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})"
      hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
      with that have "(SUP X\<in>A. count X i) \<le> 0"
        by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto
      with pos show False by simp
    qed
  qed
  moreover from that have "finite \<dots>"
    by (rule bdd_above_multiset_imp_finite_support)
  ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}"
    by (rule finite_subset)
qed

lemma count_Sup_multiset_nonempty:
  \<open>count (Sup A) x = (SUP X\<in>A. count X x)\<close>
  if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
  using that by (simp add: Sup_multiset_def Sup_multiset_in_multiset count_Abs_multiset)

interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
proof
  fix X :: "'a multiset" and A
  assume "X \<in> A"
  show "Inf A \<subseteq># X"
  proof (rule mset_subset_eqI)
    fix x
    from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
    hence "count (Inf A) x = (INF X\<in>A. count X x)"
      by (simp add: count_Inf_multiset_nonempty)
    also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
      by (intro cInf_lower) simp_all
    finally show "count (Inf A) x \<le> count X x" .
  qed
next
  fix X :: "'a multiset" and A
  assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y"
  show "X \<subseteq># Inf A"