(* 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.61 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
