Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 3 kB

Impressum Multiset.thy Sprache: Isabelle

(*  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 = \{f :: 'a \ nat. finite {x. f x > 0}}\
  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 \ (\a. count M a = count N a)"
  by (simp only: count_inject [symmetric] fun_eq_iff)

lemma multiset_eqI: "(\x. count A x = count B x) \ 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 \ bool" where
  [code_abbrev]: "is_empty A \ 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 \ 'a multiset \ 'a multiset" is
  "\a M b. if b = a then Suc (M b) else M b"
by (rule add_mset_in_multiset)

syntax
  "_multiset" :: "args \ 'a multiset" (\(\indent=2 notation=\mixfix multiset enumeration\\{#_#})\)
syntax_consts
  "_multiset" \<rightleftharpoons> add_mset
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]: "{#} \ 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 \ 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>(\<open>notation=\<open>infix \<in>#\<close>\<close>_/ \<in># _)\<close> [50, 51] 50)

notation  (ASCII)
  member_mset  (\<open>'(:#')\<close>) and
  member_mset  (\<open>(\<open>notation=\<open>infix :#\<close>\<close>_/ :# _)\<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>(\<open>notation=\<open>infix \<notin>#\<close>\<close>_/ \<notin># _)\<close> [50, 51] 50)

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

context
begin

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

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

end

syntax
  "_MBall"       :: "pttrn \ 'a set \ bool \ bool"
    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<in>#_./ _)\<close> [0, 0, 10] 10)
  "_MBex"        :: "pttrn \ 'a set \ bool \ bool"
    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<in>#_./ _)\<close> [0, 0, 10] 10)
syntax  (ASCII)
  "_MBall"       :: "pttrn \ 'a set \ bool \ bool"
    (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_:#_./ _)\<close> [0, 0, 10] 10)
  "_MBex"        :: "pttrn \ 'a set \ bool \ bool"
    (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_:#_./ _)\<close> [0, 0, 10] 10)
syntax_consts
  "_MBall" \<rightleftharpoons> Multiset.Ball and
  "_MBex" \<rightleftharpoons> Multiset.Bex
translations
  "\x\#A. P" \ "CONST Multiset.Ball A (\x. P)"
  "\x\#A. P" \ "CONST Multiset.Bex A (\x. P)"

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

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

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

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

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

lemma in_countE:
  assumes "x \# 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 \ Suc 0 \ x \# M"
  by (simp add: Suc_le_eq)

lemma count_greater_eq_one_iff [simp]:
  "count M x \ 1 \ x \# 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 = {} \ 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 \ {#}"
  obtains x where "x \# A"
proof -
  have "\x. x \# A" by (rule ccontr) (insert assms, auto)
  with that show ?thesis by blast
qed

lemma count_gt_imp_in_mset: "count M x > n \ x \# M"
  using count_greater_zero_iff by fastforce

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

(* TODO: reverse arguments to prevent unfolding loop *)
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 \# M - N \ count N a < count M a"
  by (simp add: set_mset_def)

lemma count_in_diffI:
  assumes "\n. count N x = n + count M x \ False"
  shows "x \# M - N"
proof (rule ccontr)
  assume "x \# 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 \# 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 \# M - N"
  shows "a \# M"
proof -
  have "0 \ 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 \ {#} - 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 \# M \ add_mset x (M - {#x#}) = M"
  by (clarsimp simp: multiset_eq_iff)

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

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

lemma diff_add_mset_swap [simp]: "b \# A \ 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 \# M \ 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 \# J \ I + J - {#a#} = I + (J - {#a#})"
  by (simp add: multiset_eq_iff Suc_le_eq)

lemma mset_add [elim?]:
  assumes "a \# 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 \# A + B \ a \# A \ a \# B"
  by auto

lemma count_minus_inter_lt_count_minus_inter_iff:
  "count (M2 - M1) y < count (M1 - M2) y \ y \# M1 - M2"
  by (meson count_greater_zero_iff gr_implies_not_zero in_diff_count leI order.strict_trans2
      order_less_asym)

lemma minus_inter_eq_minus_inter_iff:
  "(M1 - M2) = (M2 - M1) \ set_mset (M1 - M2) = set_mset (M2 - M1)"
  by (metis add.commute count_diff count_eq_zero_iff diff_add_zero in_diff_countE multiset_eq_iff)

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

abbreviation Min_mset :: "'a::linorder multiset \ 'a" where
"Min_mset m \ Min (set_mset m)"

abbreviation Max_mset :: "'a::linorder multiset \ 'a" where
"Max_mset m \ Max (set_mset m)"

lemma
  Min_in_mset: "M \ {#} \ Min_mset M \# M" and
  Max_in_mset: "M \ {#} \ Max_mset M \# M"
  by simp+

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

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

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

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

lemma multi_self_add_other_not_self [simp]: "M = add_mset x M \ 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: "\ x \# M \ M - {#x#} = M"
  by (auto simp add: multiset_eq_iff not_in_iff)

lemma diff_single_eq_union: "x \# M \ M - {#x#} = N \ M = add_mset x N"
  by auto

lemma union_single_eq_diff: "add_mset x M = N \ 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 \ x \# N"
  by auto

lemma add_mset_remove_trivial_If:
  "add_mset a (N - {#a#}) = (if a \# 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#} \ M = {#a#} \ N = {#} \ M = {#} \ 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 \ {#a#} = M \ N = {#} \ M = {#} \ {#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 \ M = N \ a = b \ M = add_mset b (N - {#a#}) \ N = add_mset a (M - {#b#})"
  (is "?lhs \ ?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 \# 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#} \ b = a \ M = {#}"
  by (auto simp: add_eq_conv_diff)

lemma single_eq_add_mset [iff]: "{#a#} = add_mset b M \ b = a \ 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 \ c"
  shows "c \# B"
proof -
  have "c \# add_mset c C" by simp
  have nc: "\ c \# {#b#}" using bnotc by simp
  then have "c \# add_mset b B" using BC by simp
  then show "c \# 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 \# M \ \A. M = add_mset x A"
  by (rule exI [where x = "M - {#x#}"]) simp

lemma multiset_add_sub_el_shuffle:
  assumes "c \# B"
    and "b \ 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#} \ M = {#} \ x = y"
  by auto

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

definition subseteq_mset :: "'a multiset \ 'a multiset \ bool" (infix \\#\ 50)
  where "A \# B \ (\a. count A a \ count B a)"

definition subset_mset :: "'a multiset \ 'a multiset \ bool" (infix \\#\ 50)
  where "A \# B \ A \# B \ A \ B"

abbreviation (input) supseteq_mset :: "'a multiset \ 'a multiset \ bool" (infix \\#\ 50)
  where "supseteq_mset A B \ B \# A"

abbreviation (input) supset_mset :: "'a multiset \ 'a multiset \ bool" (infix \\#\ 50)
  where "supset_mset A B \ B \# A"

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

notation (ASCII)
  subseteq_mset  (infix \<open><=#\<close> 50) and
  subset_mset  (infix \<open><#\<close> 50) and
  supseteq_mset  (infix \<open>>=#\<close> 50) and
  supset_mset  (infix \<open>>#\<close> 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 "(-)" "(\#)" "(\#)"
  by standard
    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

lemma mset_subset_eqI:
  "(\a. count A a \ count B a) \ A \# B"
  by (simp add: subseteq_mset_def)

lemma mset_subset_eq_count:
  "A \# B \ count A a \ count B a"
  by (simp add: subseteq_mset_def)

lemma mset_subset_eq_exists_conv: "(A::'a multiset) \# B \ (\C. B = A + C)"
  unfolding subseteq_mset_def
  by (metis add_diff_cancel_left' count_diff count_union le_Suc_ex le_add_same_cancel1 multiset_eq_iff zero_le)

interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\#)" "(\#)" "(-)"
  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 \# B + C \ A \# B"
   by (fact subset_mset.add_le_cancel_right)

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

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

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

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

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

lemma mset_subset_eq_single: "a \# B \ {#a#} \# 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 \# B \ 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 \# A \ A - B + C = A + C - B"
  by (fact subset_mset.add_diff_assoc2)

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

lemma mset_subset_eqD:
  assumes "A \# B" and "x \# A"
  shows "x \# 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 \# B \ x \# A \ x \# B"
  by (auto intro: mset_subset_eqD [of A])

lemma set_mset_mono:
  "A \# B \ set_mset A \ set_mset B"
  by (metis mset_subset_eqD subsetI)

lemma mset_subset_eq_insertD:
  assumes "add_mset x A \# B"
  shows "x \# B \ A \# B"
proof
  show "x \# B"
    using assms by (simp add: mset_subset_eqD)
  have "A \# add_mset x A"
    by (metis (no_types) add_mset_add_single mset_subset_eq_add_left)
  then have "A \# add_mset x A"
    by (meson multi_self_add_other_not_self subset_mset.le_imp_less_or_eq)
  then show "A \# B"
    using assms subset_mset.strict_trans2 by blast
qed

lemma mset_subset_insertD:
  "add_mset x A \# B \ x \# B \ A \# B"
  by (rule mset_subset_eq_insertD) simp

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

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

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

lemma insert_subset_eq_iff:
  "add_mset a A \# B \ a \# B \ A \# B - {#a#}"
  using mset_subset_eq_insertD subset_mset.le_diff_conv2 by fastforce

lemma insert_union_subset_iff:
  "add_mset a A \# B \ a \# B \ A \# B - {#a#}"
  by (auto simp add: insert_subset_eq_iff subset_mset_def)

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

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

lemma multi_psub_self: "A \# A = False"
  by simp

lemma mset_subset_add_mset [simp]: "add_mset x N \# add_mset x M \ N \# 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 \# B \ B - {#c#} \# B"
  by (auto simp: subset_mset_def elim: mset_add)

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

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

lemma nonempty_subseteq_mset_eq_single: "M \ {#} \ M \# {#x#} \ M = {#x#}"
  by (cases M) (metis single_is_union subset_mset.less_eqE)

lemma nonempty_subseteq_mset_iff_single: "(M \ {#} \ M \# {#x#} \ P) \ M = {#x#} \ P"
  by (cases M) (metis empty_not_add_mset nonempty_subseteq_mset_eq_single subset_mset.order_refl)

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>
proof
  show "\a b. (b \# a) = (a = a \# b)"
    by (simp add: Diff_eq_empty_iff_mset union_mset_def)
  show "\a b. (b \# a) = (a = a \# b \ a \ b)"
    by (metis Diff_eq_empty_iff_mset add_cancel_left_right subset_mset_def union_mset_def)
qed (auto simp: multiset_eqI union_mset_def)

interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
proof -
  have [simp]: "m \ n \ q \ n \ m + (q - m) \ n" for m n q :: nat
    by arith
  show "class.semilattice_sup (\#) (\#) (\#)"
    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 "(\#)" "(\#)" "(\#)"
  "(\#)" "{#}"
  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 \# B) = set_mset A \ set_mset B"
  by (simp only: set_mset_def) auto

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

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

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

lemma multiset_union_diff_commute:
  assumes "B \# 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 \ 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 \# B = {#} \ (\a. a \# A \ a \# B)"
  by (metis disjoint_iff set_mset_eq_empty_iff set_mset_inter)

lemma inter_mset_empty_distrib_right: "A \# (B + C) = {#} \ A \# B = {#} \ A \# C = {#}"
  by (meson disjunct_not_in union_iff)

lemma inter_mset_empty_distrib_left: "(A + B) \# C = {#} \ A \# C = {#} \ B \# C = {#}"
  by (meson disjunct_not_in union_iff)

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

lemma add_mset_disjoint [simp]:
  "add_mset a A \# B = {#} \ a \# B \ A \# B = {#}"
  "{#} = add_mset a A \# B \ a \# B \ {#} = A \# B"
  by (auto simp: disjunct_not_in)

lemma disjoint_add_mset [simp]:
  "B \# add_mset a A = {#} \ a \# B \ B \# A = {#}"
  "{#} = A \# add_mset b B \ b \# A \ {#} = A \# B"
  by (auto simp: disjunct_not_in)

lemma inter_add_left1: "\ x \# N \ (add_mset x M) \# N = M \# N"
  by (simp add: multiset_eq_iff not_in_iff)

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

lemma inter_add_right1: "\ x \# N \ N \# (add_mset x M) = N \# M"
  by (simp add: multiset_eq_iff not_in_iff)

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

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

lemma at_most_one_mset_mset_diff:
  assumes "a \# 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 \# M - {#a#}"
  shows "set_mset (M - {#a#}) = set_mset M"
proof (rule set_eqI)
  fix b
  have "Suc 0 < count M b \ count M b > 0" by arith
  then show "b \# M - {#a#} \ b \# M"
    using assms by (auto simp add: in_diff_count)
qed

lemma inter_iff:
  "a \# A \# B \ a \# A \ a \# B"
  by simp

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

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

lemma inter_subset_eq_union:
  "A \# B \# 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]: "\ x \# N \ (add_mset x M) \# N = add_mset x (M \# N)"
  by (simp add: multiset_eq_iff not_in_iff)

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

lemma sup_union_right1 [simp]: "\ x \# N \ N \# (add_mset x M) = add_mset x (N \# M)"
  by (simp add: multiset_eq_iff not_in_iff)

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

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

lemma union_sup_distrib_right:
  "C + A \# B = (C + A) \# (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 \# B = A \# B"
  by (auto simp add: multiset_eq_iff)

lemma union_diff_sup_eq_inter:
  "A + B - A \# B = A \# 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 \ 'a \ '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': \repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\
  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

lemma set_mset_sum: "finite A \ set_mset (\x\A. f x) = (\x\A. set_mset (f x))"
  by (induction A rule: finite_induct) auto

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 \ (i::nat) \ (repeat_mset i u + m \# repeat_mset j u + n) = (repeat_mset (i-j) u + m \# n)"
  by (auto simp add: subseteq_mset_def nat_le_add_iff1)

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

lemma mset_subset_add_iff1:
  "j \ (i::nat) \ (repeat_mset i u + m \# repeat_mset j u + n) = (repeat_mset (i-j) u + m \# 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 \ (j::nat) \ (repeat_mset i u + m \# repeat_mset j u + n) = (m \# 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>K Cancel_Simprocs.eq_cancel\<close>

simproc_setup msetsubset_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>K Multiset_Simprocs.subset_cancel_msets\<close>

simproc_setup msetsubset_eq_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>K 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>K Cancel_Simprocs.diff_cancel\<close>

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

instantiation multiset :: (type) Inf
begin

lift_definition Inf_multiset :: "'a multiset set \ 'a multiset" is
  "\A i. if A = {} then 0 else Inf ((\f. f i) ` A)"
proof -
  fix A :: "('a \ nat) set"
  assume *: "\f. f \ A \ 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 \ A" by blast
    hence "{i. Inf ((\f. f i) ` A) > 0} \ {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 ((\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 \ {} \ count (Inf A) x = Inf ((\X. count X x) ` A)"
  by transfer simp_all

instantiation multiset :: (type) Sup
begin

definition Sup_multiset :: "'a multiset set \ 'a multiset" where
  "Sup_multiset A = (if A \ {} \ 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: "\ subset_mset.bdd_above A \ 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 ((\X. count X x) ` A)"
proof -
  from assms obtain Y where Y: "\X\A. X \# Y"
    by (meson subset_mset.bdd_above.E)
  hence "count X x \ count Y x" if "X \ 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 \ {}" "subset_mset.bdd_above (A :: 'a multiset set)"
  shows   "finite (\X\A. {x. count X x > 0})"
proof -
  from assms obtain Y where Y: "\X\A. X \# Y"
    by (meson subset_mset.bdd_above.E)
  hence "count X x \ count Y x" if "X \ A" for X x
    using that by (auto intro: mset_subset_eq_count)
  hence "(\X\A. {x. count X x > 0}) \ {x. count Y x > 0}"
    by safe (erule less_le_trans)
  moreover have "finite \" 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 ((\X. count X i) ` A) > 0} \ (\X\A. {i. 0 < count X i})"
  proof safe
    fix i assume pos: "(SUP X\A. count X i) > 0"
    show "i \ (\X\A. {i. 0 < count X i})"
    proof (rule ccontr)
      assume "i \ (\X\A. {i. 0 < count X i})"
      hence "\X\A. count X i \ 0" by (auto simp: count_eq_zero_iff)
      with that have "(SUP X\A. count X i) \ 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 \"
    by (rule bdd_above_multiset_imp_finite_support)
  ultimately show "finite {i. Sup ((\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 "(\#)" "(\#)" "(\#)" "(\#)"
proof
  fix X :: "'a multiset" and A
  assume "X \ A"
  show "Inf A \# X"
    by (metis \<open>X \<in> A\<close> count_Inf_multiset_nonempty empty_iff image_eqI mset_subset_eqI wellorder_Inf_le1)
next
  fix X :: "'a multiset" and A
  assume nonempty: "A \ {}" and le: "\Y. Y \ A \ X \# Y"
  show "X \# Inf A"
  proof (rule mset_subset_eqI)
    fix x
    from nonempty have "count X x \ (INF X\A. count X x)"
      by (intro cInf_greatest) (auto intro: mset_subset_eq_count le)
    also from nonempty have "\ = count (Inf A) x" by (simp add: count_Inf_multiset_nonempty)
    finally show "count X x \ count (Inf A) x" .
  qed
next
  fix X :: "'a multiset" and A
  assume X: "X \ A" and bdd: "subset_mset.bdd_above A"
  show "X \# Sup A"
  proof (rule mset_subset_eqI)
    fix x
    from X have "A \ {}" by auto
    have "count X x \ (SUP X\A. count X x)"
      by (intro cSUP_upper X bdd_above_multiset_imp_bdd_above_count bdd)
    also from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
      have "(SUP X\A. count X x) = count (Sup A) x" by simp
    finally show "count X x \ count (Sup A) x" .
  qed
next
  fix X :: "'a multiset" and A
  assume nonempty: "A \ {}" and ge: "\Y. Y \ A \ Y \# X"
  from ge have bdd: "subset_mset.bdd_above A"
    by blast
  show "Sup A \# X"
  proof (rule mset_subset_eqI)
    fix x
    from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
      have "count (Sup A) x = (SUP X\A. count X x)" .
    also from nonempty have "\ \ count X x"
      by (intro cSup_least) (auto intro: mset_subset_eq_count ge)
    finally show "count (Sup A) x \ count X x" .
  qed
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

lemma set_mset_Inf:
  assumes "A \ {}"
  shows   "set_mset (Inf A) = (\X\A. set_mset X)"
proof safe
  fix x X assume "x \# Inf A" "X \ A"
  hence nonempty: "A \ {}" by (auto simp: Inf_multiset_empty)
  from \<open>x \<in># Inf A\<close> have "{#x#} \<subseteq># Inf A" by auto
  also from \<open>X \<in> A\<close> have "\<dots> \<subseteq># X" by (rule subset_mset.cInf_lower) simp_all
  finally show "x \# X" by simp
next
  fix x assume x: "x \ (\X\A. set_mset X)"
  hence "{#x#} \# X" if "X \ A" for X using that by auto
  from assms and this have "{#x#} \# Inf A" by (rule subset_mset.cInf_greatest)
  thus "x \# Inf A" by simp
qed

lemma in_Inf_multiset_iff:
  assumes "A \ {}"
  shows   "x \# Inf A \ (\X\A. x \# X)"
proof -
  from assms have "set_mset (Inf A) = (\X\A. set_mset X)" by (rule set_mset_Inf)
  also have "x \ \ \ (\X\A. x \# X)" by simp
  finally show ?thesis .
qed

lemma in_Inf_multisetD: "x \# Inf A \ X \ A \ x \# X"
  by (subst (asm) in_Inf_multiset_iff) auto

lemma set_mset_Sup:
  assumes "subset_mset.bdd_above A"
  shows   "set_mset (Sup A) = (\X\A. set_mset X)"
proof safe
  fix x assume "x \# Sup A"
  hence nonempty: "A \ {}" by (auto simp: Sup_multiset_empty)
  show "x \ (\X\A. set_mset X)"
  proof (rule ccontr)
    assume x: "x \ (\X\A. set_mset X)"
    have "count X x \ count (Sup A) x" if "X \ A" for X x
      using that by (intro mset_subset_eq_count subset_mset.cSup_upper assms)
    with x have "X \# Sup A - {#x#}" if "X \ A" for X
      using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
    hence "Sup A \# Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
    with \<open>x \<in># Sup A\<close> show False
      using mset_subset_diff_self by fastforce
  qed
next
  fix x X assume "x \ set_mset X" "X \ A"
  hence "{#x#} \# X" by auto
  also have "X \# Sup A" by (intro subset_mset.cSup_upper \X \ A\ assms)
  finally show "x \ set_mset (Sup A)" by simp
qed

lemma in_Sup_multiset_iff:
  assumes "subset_mset.bdd_above A"
  shows   "x \# Sup A \ (\X\A. x \# X)"
  by (simp add: assms set_mset_Sup)

lemma in_Sup_multisetD:
  assumes "x \# Sup A"
  shows   "\X\A. x \# X"
  using Sup_multiset_unbounded assms in_Sup_multiset_iff by fastforce

interpretation subset_mset: distrib_lattice "(\#)" "(\#)" "(\#)" "(\#)"
proof
  fix A B C :: "'a multiset"
  show "A \# (B \# C) = A \# B \# (A \# C)"
    by (intro multiset_eqI) simp_all
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

subsubsection \<open>Filter (with comprehension syntax)\<close>

text \<open>Multiset comprehension\<close>

lift_definition filter_mset :: "('a \ bool) \ 'a multiset \ 'a multiset"
is "\P M. \x. if P x then M x else 0"
by (rule filter_preserves_multiset)

syntax (ASCII)
  "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset"
    (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ :# _./ _#})\<close>)
syntax
  "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset"
    (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ \<in># _./ _#})\<close>)
syntax_consts
  "_MCollect" == filter_mset
translations
  "{#x \# M. P#}" == "CONST filter_mset (\x. P) M"

lemma count_filter_mset [simp]:
  "count (filter_mset P M) a = (if P a then count M a else 0)"
  by (simp add: filter_mset.rep_eq)

lemma set_mset_filter [simp]:
  "set_mset (filter_mset P M) = {a \ set_mset M. P a}"
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_filter_mset) simp

lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}"
  by (rule multiset_eqI) simp

lemma filter_single_mset: "filter_mset P {#x#} = (if P x then {#x#} else {#})"
  by (rule multiset_eqI) simp

lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
  by (rule multiset_eqI) simp

lemma filter_diff_mset [simp]: "filter_mset P (M - N) = filter_mset P M - filter_mset P N"
  by (rule multiset_eqI) simp

lemma filter_inter_mset [simp]: "filter_mset P (M \# N) = filter_mset P M \# filter_mset P N"
  by (rule multiset_eqI) simp

lemma filter_sup_mset[simp]: "filter_mset P (A \# B) = filter_mset P A \# filter_mset P B"
  by (rule multiset_eqI) simp

lemma filter_mset_add_mset [simp]:
   "filter_mset P (add_mset x A) =
     (if P x then add_mset x (filter_mset P A) else filter_mset P A)"
   by (auto simp: multiset_eq_iff)

lemma multiset_filter_subset[simp]: "filter_mset f M \# M"
  by (simp add: mset_subset_eqI)

lemma filter_mset_mono_strong:
  assumes "A \# B" "\x. x \# A \ P x \ Q x"
  shows   "filter_mset P A \# filter_mset Q B"
  by (rule mset_subset_eqI) (insert assms, auto simp: mset_subset_eq_count count_eq_zero_iff)

(* TODO: rename to filter_mset_mono_strong *)
lemma multiset_filter_mono:
  assumes "A \# B"
  shows "filter_mset f A \# filter_mset f B"
  using filter_mset_mono_strong[OF \<open>A \<subseteq># B\<close>] .

lemma filter_mset_eq_conv:
  "filter_mset P M = N \ N \# M \ (\b\#N. P b) \ (\a\#M - N. \ P a)" (is "?P \ ?Q")
proof
  assume ?P then show ?Q by auto (simp add: multiset_eq_iff in_diff_count)
next
  assume ?Q
  then obtain Q where M: "M = N + Q"
    by (auto simp add: mset_subset_eq_exists_conv)
  then have MN: "M - N = Q" by simp
  show ?P
  proof (rule multiset_eqI)
    fix a
    from \<open>?Q\<close> MN have *: "\<not> P a \<Longrightarrow> a \<notin># N" "P a \<Longrightarrow> a \<notin># Q"
      by auto
    show "count (filter_mset P M) a = count N a"
    proof (cases "a \# M")
      case True
      with * show ?thesis
        by (simp add: not_in_iff M)
    next
      case False then have "count M a = 0"
        by (simp add: not_in_iff)
      with M show ?thesis by simp
    qed
  qed
qed

lemma filter_mset_eq_mempty_iff[simp]: "filter_mset P A = {#} \ (\x. x \# A \ \ P x)"
  by (auto simp: multiset_eq_iff count_eq_zero_iff)

lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \# M. Q x \ P x#}"
  by (auto simp: multiset_eq_iff)

lemma
  filter_mset_True[simp]: "{#y \# M. True#} = M" and
  filter_mset_False[simp]: "{#y \# M. False#} = {#}"
  by (auto simp: multiset_eq_iff)

lemma filter_mset_cong0:
  assumes "\x. x \# M \ f x \ g x"
  shows "filter_mset f M = filter_mset g M"
proof (rule subset_mset.antisym; unfold subseteq_mset_def; rule allI)
  fix x
  show "count (filter_mset f M) x \ count (filter_mset g M) x"
    using assms by (cases "x \# M") (simp_all add: not_in_iff)
next
  fix x
  show "count (filter_mset g M) x \ count (filter_mset f M) x"
    using assms by (cases "x \# M") (simp_all add: not_in_iff)
qed

lemma filter_mset_cong:
  assumes "M = M'" and "\x. x \# M' \ f x \ g x"
  shows "filter_mset f M = filter_mset g M'"
  unfolding \<open>M = M'\<close>
  using assms by (auto intro: filter_mset_cong0)

lemma filter_eq_replicate_mset: "{#y \# D. y = x#} = replicate_mset (count D x) x"
  by (induct D) (simp add: multiset_eqI)

subsubsection \<open>Size\<close>

definition wcount where "wcount f M = (\x. count M x * Suc (f x))"

lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
  by (auto simp: wcount_def add_mult_distrib)

lemma wcount_add_mset:
  "wcount f (add_mset x M) a = (if x = a then Suc (f a) else 0) + wcount f M a"
  unfolding add_mset_add_single[of _ M] wcount_union by (auto simp: wcount_def)

definition size_multiset :: "('a \ nat) \ 'a multiset \ nat" where
  "size_multiset f M = sum (wcount f M) (set_mset M)"

lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]

instantiation multiset :: (type) size
begin

definition size_multiset where
  size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\_. 0)"
instance ..

end

lemmas size_multiset_overloaded_eq =
  size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]

lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
  by (simp add: size_multiset_def)

lemma size_empty [simp]: "size {#} = 0"
  by (simp add: size_multiset_overloaded_def)

lemma size_multiset_single : "size_multiset f {#b#} = Suc (f b)"
  by (simp add: size_multiset_eq)

lemma size_single: "size {#b#} = 1"
  by (simp add: size_multiset_overloaded_def size_multiset_single)

lemma sum_wcount_Int:
  "finite A \ sum (wcount f N) (A \ set_mset N) = sum (wcount f N) A"
  by (induct rule: finite_induct)
    (simp_all add: Int_insert_left wcount_def count_eq_zero_iff)

lemma size_multiset_union [simp]:
  "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
  apply (simp add: size_multiset_def sum_Un_nat sum.distrib sum_wcount_Int wcount_union)
  by (metis add_implies_diff finite_set_mset inf.commute sum_wcount_Int)

lemma size_multiset_add_mset [simp]:
  "size_multiset f (add_mset a M) = Suc (f a) + size_multiset f M"
  by (metis add.commute add_mset_add_single size_multiset_single size_multiset_union)

lemma size_add_mset [simp]: "size (add_mset a A) = Suc (size A)"
  by (simp add: size_multiset_overloaded_def wcount_add_mset)

lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
  by (auto simp add: size_multiset_overloaded_def)

lemma size_multiset_eq_0_iff_empty [iff]:
  "size_multiset f M = 0 \ M = {#}"
  by (auto simp add: size_multiset_eq count_eq_zero_iff)

lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
by (auto simp add: size_multiset_overloaded_def)

lemma nonempty_has_size: "(S \ {#}) = (0 < size S)"
  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)

lemma size_eq_Suc_imp_elem: "size M = Suc n \ \a. a \# M"
  using all_not_in_conv by fastforce

lemma size_eq_Suc_imp_eq_union:
  assumes "size M = Suc n"
  shows "\a N. M = add_mset a N"
  by (metis assms insert_DiffM size_eq_Suc_imp_elem)

lemma size_mset_mono:
  fixes A B :: "'a multiset"
  assumes "A \# B"
  shows "size A \ size B"
proof -
  from assms[unfolded mset_subset_eq_exists_conv]
  obtain C where B: "B = A + C" by auto
  show ?thesis unfolding B by (induct C) auto
qed

lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \ size M"
  by (rule size_mset_mono[OF multiset_filter_subset])

lemma size_Diff_submset:
  "M \# M' \ size (M' - M) = size M' - size(M::'a multiset)"
by (metis add_diff_cancel_left' size_union mset_subset_eq_exists_conv)

lemma size_lt_imp_ex_count_lt: "size M < size N \ \x \# N. count M x < count N x"
  by (metis count_eq_zero_iff leD not_le_imp_less not_less_zero size_mset_mono subseteq_mset_def)

subsection \<open>Induction and case splits\<close>

theorem multiset_induct [case_names empty add, induct type: multiset]:
  assumes empty: "P {#}"
  assumes add: "\x M. P M \ P (add_mset x M)"
  shows "P M"
proof (induct "size M" arbitrary: M)
  case 0 thus "P M" by (simp add: empty)
next
  case (Suc k)
  obtain N x where "M = add_mset x N"
    using \<open>Suc k = size M\<close> [symmetric]
    using size_eq_Suc_imp_eq_union by fast
  with Suc add show "P M" by simp
qed

lemma multiset_induct_min[case_names empty add]:
  fixes M :: "'a::linorder multiset"
  assumes
    empty: "P {#}" and
    add: "\x M. P M \ (\y \# M. y \ x) \ P (add_mset x M)"
  shows "P M"
proof (induct "size M" arbitrary: M)
  case (Suc k)
  note ih = this(1) and Sk_eq_sz_M = this(2)

  let ?y = "Min_mset M"
  let ?N = "M - {#?y#}"

  have M: "M = add_mset ?y ?N"
    by (metis Min_in Sk_eq_sz_M finite_set_mset insert_DiffM lessI not_less_zero
      set_mset_eq_empty_iff size_empty)
  show ?case
    by (subst M, rule add, rule ih, metis M Sk_eq_sz_M nat.inject size_add_mset,
      meson Min_le finite_set_mset in_diffD)
qed (simp add: empty)

lemma multiset_induct_max[case_names empty add]:
  fixes M :: "'a::linorder multiset"
  assumes
    empty: "P {#}" and
    add: "\x M. P M \ (\y \# M. y \ x) \ P (add_mset x M)"
  shows "P M"
proof (induct "size M" arbitrary: M)
  case (Suc k)
  note ih = this(1) and Sk_eq_sz_M = this(2)

  let ?y = "Max_mset M"
  let ?N = "M - {#?y#}"

  have M: "M = add_mset ?y ?N"
    by (metis Max_in Sk_eq_sz_M finite_set_mset insert_DiffM lessI not_less_zero
      set_mset_eq_empty_iff size_empty)
  show ?case
    by (subst M, rule add, rule ih, metis M Sk_eq_sz_M nat.inject size_add_mset,
      meson Max_ge finite_set_mset in_diffD)
qed (simp add: empty)

lemma multi_nonempty_split: "M \ {#} \ \A a. M = add_mset a A"
  by (induct M) auto

lemma multiset_cases [cases type]:
  obtains (empty) "M = {#}" | (add) x N where "M = add_mset x N"
  by (induct M) simp_all

lemma multi_drop_mem_not_eq: "c \# B \ B - {#c#} \ B"
  by (cases "B = {#}") (auto dest: multi_member_split)

lemma union_filter_mset_complement[simp]:
  "\x. P x = (\ Q x) \ filter_mset P M + filter_mset Q M = M"
  by (subst multiset_eq_iff) auto

lemma multiset_partition: "M = {#x \# M. P x#} + {#x \# M. \ P x#}"
  by simp

lemma mset_subset_size: "A \# B \ size A < size B"
proof (induct A arbitrary: B)
  case empty
  then show ?case
    using nonempty_has_size by auto
next
  case (add x A)
  have "add_mset x A \# B"
    by (meson add.prems subset_mset_def)
  then show ?case
    using add.prems subset_mset.less_eqE by fastforce
qed

lemma size_1_singleton_mset: "size M = 1 \ \a. M = {#a#}"
  by (cases M) auto

lemma set_mset_subset_singletonD:
  assumes "set_mset A \ {x}"
  shows   "A = replicate_mset (size A) x"
  using assms by (induction A) auto

lemma count_conv_size_mset: "count A x = size (filter_mset (\y. y = x) A)"
  by (induction A) auto

lemma size_conv_count_bool_mset: "size A = count A True + count A False"
  by (induction A) auto

subsubsection \<open>Strong induction and subset induction for multisets\<close>

text \<open>Well-foundedness of strict subset relation\<close>

lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \# N}"
  using mset_subset_size wfp_def wfp_if_convertible_to_nat by blast

lemma wfp_subset_mset[simp]: "wfp (\#)"
  by (rule wf_subset_mset_rel[to_pred])

lemma full_multiset_induct [case_names less]:
  assumes ih: "\B. \(A::'a multiset). A \# B \ P A \ P B"
  shows "P B"
  apply (rule wf_subset_mset_rel [THEN wf_induct])
  apply (rule ih, auto)
  done

lemma multi_subset_induct [consumes 2, case_names empty add]:
  assumes "F \# A"
    and empty: "P {#}"
    and insert: "\a F. a \# A \ P F \ P (add_mset a F)"
  shows "P F"
proof -
  from \<open>F \<subseteq># A\<close>
  show ?thesis
  proof (induct F)
    show "P {#}" by fact
  next
    fix x F
    assume P: "F \# A \ P F" and i: "add_mset x F \# A"
    show "P (add_mset x F)"
    proof (rule insert)
      from i show "x \# A" by (auto dest: mset_subset_eq_insertD)
      from i have "F \# A" by (auto dest: mset_subset_eq_insertD)
      with P show "P F" .
    qed
  qed
qed

subsection \<open>Least and greatest elements\<close>

context begin

qualified lemma
  assumes
    "M \ {#}" and
    "transp_on (set_mset M) R" and
    "totalp_on (set_mset M) R"
  shows
    bex_least_element: "(\l \# M. \x \# M. x \ l \ R l x)" and
    bex_greatest_element: "(\g \# M. \x \# M. x \ g \ R x g)"
  using assms
  by (auto intro: Finite_Set.bex_least_element Finite_Set.bex_greatest_element)

end

subsection \<open>The fold combinator\<close>

definition fold_mset :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b"
where
  "fold_mset f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_mset M)"

lemma fold_mset_empty [simp]: "fold_mset f s {#} = s"
  by (simp add: fold_mset_def)

lemma fold_mset_single [simp]: "fold_mset f s {#x#} = f x s"
  by (simp add: fold_mset_def)

context comp_fun_commute
begin

lemma fold_mset_add_mset [simp]: "fold_mset f s (add_mset x M) = f x (fold_mset f s M)"
proof -
  interpret mset: comp_fun_commute "\y. f y ^^ count M y"
    by (fact comp_fun_commute_funpow)
  interpret mset_union: comp_fun_commute "\y. f y ^^ count (add_mset x M) y"
    by (fact comp_fun_commute_funpow)
  show ?thesis
  proof (cases "x \ set_mset M")
    case False
    then have *: "count (add_mset x M) x = 1"
      by (simp add: not_in_iff)
    from False have "Finite_Set.fold (\y. f y ^^ count (add_mset x M) y) s (set_mset M) =
      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_on_funpow)
    with False * show ?thesis
      by (simp add: fold_mset_def del: count_add_mset)
  next
    case True
    define N where "N = set_mset M - {x}"
    from N_def True have *: "set_mset M = insert x N" "x \ N" "finite N" by auto
    then have "Finite_Set.fold (\y. f y ^^ count (add_mset x M) y) s N =
      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_on_funpow)
    with * show ?thesis by (simp add: fold_mset_def del: count_add_mset) simp
  qed
qed

lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M"
  by (induct M) (simp_all add: fun_left_comm)

lemma fold_mset_union [simp]: "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
  by (induct M) (simp_all add: fold_mset_fun_left_comm)

lemma fold_mset_fusion:
  assumes "comp_fun_commute g"
    and *: "\x y. h (g x y) = f x (h y)"
  shows "h (fold_mset g w A) = fold_mset f (h w) A"
proof -
  interpret comp_fun_commute g by (fact assms)
  from * show ?thesis by (induct A) auto
qed

end

lemma union_fold_mset_add_mset: "A + B = fold_mset add_mset A B"
proof -
  interpret comp_fun_commute add_mset
    by standard auto
  show ?thesis
    by (induction B) auto
qed

text \<open>
  A note on code generation: When defining some function containing a
  subterm \<^term>\<open>fold_mset F\<close>, code generation is not automatic. When
  interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the
--> --------------------

--> maximum size reached

--> --------------------

quality99%