Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Multiset.thy Sprache: Isabelle

Original von: 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
*)

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

theory Multiset
imports Cancellation
begin

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

definition "multiset = {f :: 'a \ nat. finite {x. f x > 0}}"

typedef 'a multiset = "multiset :: ('a \<Rightarrow> nat) set"
  morphisms count Abs_multiset
  unfolding multiset_def
proof
  show "(\x. 0::nat) \ {f. finite {x. f x > 0}}" by simp
qed

setup_lifting type_definition_multiset

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 const0_in_multiset: "(\a. 0) \ multiset"
  by (simp add: multiset_def)

lemma only1_in_multiset: "(\b. if b = a then n else 0) \ multiset"
  by (simp add: multiset_def)

lemma union_preserves_multiset: "M \ multiset \ N \ multiset \ (\a. M a + N a) \ multiset"
  by (simp add: multiset_def)

lemma diff_preserves_multiset:
  assumes "M \ multiset"
  shows "(\a. M a - N a) \ multiset"
proof -
  have "{x. N x < M x} \ {x. 0 < M x}"
    by auto
  with assms show ?thesis
    by (auto simp add: multiset_def intro: finite_subset)
qed

lemma filter_preserves_multiset:
  assumes "M \ multiset"
  shows "(\x. if P x then M x else 0) \ multiset"
proof -
  have "{x. (P x \ 0 < M x) \ P x} \ {x. 0 < M x}"
    by auto
  with assms show ?thesis
    by (auto simp add: multiset_def intro: finite_subset)
qed

lemmas in_multiset = const0_in_multiset only1_in_multiset
  union_preserves_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 :: "'a multiset" is "\a. 0"
by (rule const0_in_multiset)

abbreviation Mempty :: "'a multiset" ("{#}") where
  "Mempty \ 0"

lift_definition plus_multiset :: "'a multiset \ 'a multiset \ 'a multiset" is "\M N. (\a. M a + N a)"
by (rule union_preserves_multiset)

lift_definition minus_multiset :: "'a multiset \ 'a multiset \ 'a multiset" is "\ M N. \a. M a - N a"
by (rule diff_preserves_multiset)

instance
  by (standard; transfer; simp 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:
  assumes M: \<open>M \<in> multiset\<close>
  shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
  using assms by (simp add: multiset_def 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" ("{#(_)#}")
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 :: "'a multiset \ 'a set"
  where "set_mset M = {x. count M x > 0}"

abbreviation Melem :: "'a \ 'a multiset \ bool"
  where "Melem a M \ a \ set_mset M"

notation
  Melem  ("'(\#')") and
  Melem  ("(_/ \# _)" [51, 51] 50)

notation  (ASCII)
  Melem  ("'(:#')") and
  Melem  ("(_/ :# _)" [51, 51] 50)

abbreviation not_Melem :: "'a \ 'a multiset \ bool"
  where "not_Melem a M \ a \ set_mset M"

notation
  not_Melem  ("'(\#')") and
  not_Melem  ("(_/ \# _)" [51, 51] 50)

notation  (ASCII)
  not_Melem  ("'(~:#')") and
  not_Melem  ("(_/ ~:# _)" [51, 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" ("(3\_\#_./ _)" [0, 0, 10] 10)
  "_MBex"        :: "pttrn \ 'a set \ bool \ bool" ("(3\_\#_./ _)" [0, 0, 10] 10)

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

translations
  "\x\#A. P" \ "CONST Multiset.Ball A (\x. P)"
  "\x\#A. P" \ "CONST Multiset.Bex A (\x. P)"

print_translation \<open>
[Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\Multiset.Ball\ \<^syntax_const>\_MBall\,
  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\Multiset.Bex\ \<^syntax_const>\_MBex\]
\<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 add: multiset_def)

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

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)

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

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

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 "\#" 50) and
  supseteq_mset  (infix "\#" 50)

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

interpretation subset_mset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\#)" "(\#)"
  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
  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 "(\#)" "(\#)" "(-)"
  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:
  "add_mset x A \# B \ x \# B \ A \# 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 \# 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 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 \# 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

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

definition inf_subset_mset :: "'a multiset \ 'a multiset \ 'a multiset" (infixl "\#" 70) where
  multiset_inter_def: "inf_subset_mset A B = A - (A - B)"

interpretation subset_mset: semilattice_inf inf_subset_mset "(\#)" "(\#)"
proof -
  have [simp]: "m \ n \ m \ q \ m \ n - (n - q)" for m n q :: nat
    by arith
  show "class.semilattice_inf (\#) (\#) (\#)"
    by standard (auto simp add: multiset_inter_def subseteq_mset_def)
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>

definition sup_subset_mset :: "'a multiset \ 'a multiset \ 'a multiset"(infixl "\#" 70)
  where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>

interpretation subset_mset: semilattice_sup sup_subset_mset "(\#)" "(\#)"
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: sup_subset_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 multiset_inter_count [simp]:
  fixes A B :: "'a multiset"
  shows "count (A \# B) x = min (count A x) (count B x)"
  by (simp add: multiset_inter_def)

lemma set_mset_inter [simp]:
  "set_mset (A \# B) = set_mset A \ set_mset B"
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp

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)" (is "?P \ ?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 \ count B a = 0"
      by (cases "count A a \ count B a") (simp_all add: min_def)
    then show "a \# A \ a \# 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 \# B) a = count {#} a"
      by auto
  qed
qed

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 (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
      subset_mset.diff_add_assoc2)

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 sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close>
  "count (A \# B) x = max (count A x) (count B x)"
  by (simp add: sup_subset_mset_def)

lemma set_mset_sup [simp]:
  "set_mset (A \# B) = set_mset A \ set_mset B"
  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
    (auto simp add: not_in_iff elim: mset_add)

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

fun repeat_mset :: "nat \ 'a multiset \ 'a multiset" where
  "repeat_mset 0 _ = {#}" |
  "repeat_mset (Suc n) A = A + repeat_mset n A"

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

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 (induction n) simp_all

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>fn phi => 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>fn phi => 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>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 \ 'a multiset" is
  "\A i. if A = {} then 0 else Inf ((\f. f i) ` A)"
proof -
  fix A :: "('a \ nat) set" assume *: "\x. x \ A \ x \ multiset"
  have "finite {i. (if A = {} then 0 else Inf ((\f. f i) ` A)) > 0}" unfolding multiset_def
  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 add: multiset_def)
    ultimately have "finite {i. Inf ((\f. f i) ` A) > 0}" by (rule finite_subset)
    with False show ?thesis by simp
  qed simp_all
  thus "(\i. if A = {} then 0 else INF f\A. f i) \ multiset" by (simp add: multiset_def)
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 (auto simp: subset_mset.bdd_above_def)
  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 (auto simp: subset_mset.bdd_above_def)
  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:
  assumes "A \ {}" "subset_mset.bdd_above A"
  shows   "(\i. SUP X\A. count X i) \ multiset"
  unfolding multiset_def
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 assms 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 assms 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:
  assumes "A \ {}" "subset_mset.bdd_above A"
  shows   "count (Sup A) x = (SUP X\A. count X x)"
  using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)

interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\#)" "(\#)" "(\#)" "(\#)"
proof
  fix X :: "'a multiset" and A
  assume "X \ A"
  show "Inf A \# 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\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 \ count X x" .
  qed
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 (rule subset_mset.bdd_aboveI[of _ X])
  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
      by (auto simp: subseteq_mset_def simp flip: count_greater_zero_iff
               dest!: spec[of _ x])
  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)"
proof -
  from assms have "set_mset (Sup A) = (\X\A. set_mset X)" by (rule set_mset_Sup)
  also have "x \ \ \ (\X\A. x \# X)" by simp
  finally show ?thesis .
qed

lemma in_Sup_multisetD:
  assumes "x \# Sup A"
  shows   "\X\A. x \# X"
proof -
  have "subset_mset.bdd_above A"
    by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
  with assms show ?thesis by (simp add: in_Sup_multiset_iff)
qed

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" ("(1{#_ :# _./ _#})")
syntax
  "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{#_ \# _./ _#})")
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 multiset_filter_mono:
  assumes "A \# B"
  shows "filter_mset f A \# filter_mset f B"
proof -
  from assms[unfolded mset_subset_eq_exists_conv]
  obtain C where B: "B = A + C" by auto
  show ?thesis unfolding B by auto
qed

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

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)
apply (subst Int_commute)
apply (simp add: sum_wcount_Int)
done

lemma size_multiset_add_mset [simp]:
  "size_multiset f (add_mset a M) = Suc (f a) + size_multiset f M"
  unfolding add_mset_add_single[of _ M] size_multiset_union by (auto simp: size_multiset_single)

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"
apply (unfold size_multiset_overloaded_eq)
apply (drule sum_SucD)
apply auto
done

lemma size_eq_Suc_imp_eq_union:
  assumes "size M = Suc n"
  shows "\a N. M = add_mset a N"
proof -
  from assms obtain a where "a \# M"
    by (erule size_eq_Suc_imp_elem [THEN exE])
  then have "M = add_mset a (M - {#a#})" by simp
  then show ?thesis by blast
qed

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)

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
    by (metis (no_types) add.prems add.right_neutral add_diff_cancel_left' leD nat_neq_iff
      size_Diff_submset size_eq_0_iff_empty size_mset_mono subset_mset.le_iff_add subset_mset_def)
qed

lemma size_1_singleton_mset: "size M = 1 \ \a. M = {#a#}"
  by (cases M) 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}"
apply (rule wf_measure [THEN wf_subset, where f1=size])
apply (clarsimp simp: measure_def inv_image_def mset_subset_size)
done

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

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_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_funpow)
    with * show ?thesis by (simp add: fold_mset_def del: count_add_mset) simp
  qed
qed

corollary fold_mset_single: "fold_mset f s {#x#} = f x s"
  by simp

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
  would be code thms for \<^const>\<open>fold_mset\<close> become thms like
  \<^term>\<open>fold_mset F z {#} = z\<close> where \<open>F\<close> is not a pattern but
  contains defined symbols, i.e.\ is not a code thm. Hence a separate
  constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below.
\<close>

subsection \<open>Image\<close>

definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where
  "image_mset f = fold_mset (add_mset \ f) {#}"

lemma comp_fun_commute_mset_image: "comp_fun_commute (add_mset \ f)"
  by unfold_locales (simp add: fun_eq_iff)

lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
  by (simp add: image_mset_def)

lemma image_mset_single: "image_mset f {#x#} = {#f x#}"
  by (simp add: comp_fun_commute.fold_mset_add_mset comp_fun_commute_mset_image image_mset_def)

lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
proof -
  interpret comp_fun_commute "add_mset \ f"
    by (fact comp_fun_commute_mset_image)
  show ?thesis by (induct N) (simp_all add: image_mset_def)
qed

corollary image_mset_add_mset [simp]:
  "image_mset f (add_mset a M) = add_mset (f a) (image_mset f M)"
  unfolding image_mset_union add_mset_add_single[of a M] by (simp add: image_mset_single)

lemma set_image_mset [simp]: "set_mset (image_mset f M) = image f (set_mset M)"
  by (induct M) simp_all

lemma size_image_mset [simp]: "size (image_mset f M) = size M"
  by (induct M) simp_all

lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \ M = {#}"
  by (cases M) auto

lemma image_mset_If:
  "image_mset (\x. if P x then f x else g x) A =
     image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
  by (induction A) auto

lemma image_mset_Diff:
  assumes "B \# A"
  shows   "image_mset f (A - B) = image_mset f A - image_mset f B"
proof -
  have "image_mset f (A - B + B) = image_mset f (A - B) + image_mset f B"
    by simp
  also from assms have "A - B + B = A"
    by (simp add: subset_mset.diff_add)
  finally show ?thesis by simp
qed

lemma count_image_mset: "count (image_mset f A) x = (\y\f -` {x} \ set_mset A. count A y)"
proof (induction A)
  case empty
  then show ?case by simp
next
  case (add x A)
  moreover have *: "(if x = y then Suc n else n) = n + (if x = y then 1 else 0)" for n y
    by simp
  ultimately show ?case
    by (auto simp: sum.distrib intro!: sum.mono_neutral_left)
qed

lemma image_mset_subseteq_mono: "A \# B \ image_mset f A \# image_mset f B"
  by (metis image_mset_union subset_mset.le_iff_add)

lemma image_mset_subset_mono: "M \# N \ image_mset f M \# image_mset f N"
  by (metis (no_types) Diff_eq_empty_iff_mset image_mset_Diff image_mset_is_empty_iff
    image_mset_subseteq_mono subset_mset.less_le_not_le)

syntax (ASCII)
  "_comprehension_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ :# _#})")
syntax
  "_comprehension_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ \# _#})")
translations
  "{#e. x \# M#}" \ "CONST image_mset (\x. e) M"

syntax (ASCII)
  "_comprehension_mset'" :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" ("({#_/ | _ :# _./ _#})")
syntax
  "_comprehension_mset'" :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" ("({#_/ | _ \# _./ _#})")
translations
  "{#e | x\#M. P#}" \ "{#e. x \# {# x\#M. P#}#}"

text \<open>
  This allows to write not just filters like \<^term>\<open>{#x\<in>#M. x<c#}\<close>
  but also images like \<^term>\<open>{#x+x. x\<in>#M #}\<close> and @{term [source]
  "{#x+x|x\#M. x
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.