theory Multiset_More
imports "~~/src/HOL/Library/Multiset_Order"
begin
section ‹More about Multisets›
text ‹
Isabelle's theory of finite multisets is not as developed as other areas, such as lists and sets.
The present theory introduces some missing concepts and lemmas. Some of it is expected to move to
Isabelle's library.
›
subsection ‹Basic Setup›
declare
diff_single_trivial [simp]
ball_set_mset_iff [simp]
in_image_mset [iff]
image_mset.compositionality [simp]
mset_leD[dest, intro?]
Multiset.in_multiset_in_set[simp]
lemma image_mset_cong2[cong]:
"(⋀x. x ∈# M ⟹ f x = g x) ⟹ M = N ⟹ image_mset f M = image_mset g N"
by (hypsubst, rule image_mset_cong)
lemma subset_msetE [elim!]:
"[|A ⊂# B; [|A ⊆# B; ~ (B⊆#A)|] ==> R|] ==> R"
unfolding subseteq_mset_def subset_mset_def by (meson mset_less_eqI subset_mset.eq_iff)
abbreviation not_Melem :: "'a ⇒ 'a multiset ⇒ bool" where
"not_Melem x A ≡ ~ (x ∈# A)" ― "non-membership"
notation (ASCII)
not_Melem ("op ~:#") and
not_Melem ("(_/ ~:# _)" [51, 51] 50)
notation
not_Melem ("op ∉#") and
not_Melem ("(_/ ∉# _)" [51, 51] 50)
notation (HTML output)
not_Melem ("op ∉#") and
not_Melem ("(_/ ∉# _)" [51, 51] 50)
subsection ‹Existence and forall quantifiers in multisets›
definition Ball_mset :: "'a multiset ⇒ ('a ⇒ bool) ⇒ bool" where
"Ball_mset A P ⟷ (∀x. x ∈# A ⟶ P x)" ― "bounded universal quantifiers on multisets"
definition Bex_mset :: "'a multiset ⇒ ('a ⇒ bool) ⇒ bool" where
"Bex_mset A P ⟷ (∃x. x ∈# A ∧ P x)" ― "bounded existential quantifiers on multisets"
syntax (ASCII)
"_Ball_mset" :: "pttrn => 'a multiset => bool => bool" ("(3ALL _:#_./ _)" [0, 0, 10] 10)
"_Bex_mset" :: "pttrn => 'a multiset => bool => bool" ("(3EX _:#_./ _)" [0, 0, 10] 10)
"_Bex1_mset" :: "pttrn => 'a multiset => bool => bool" ("(3EX! _:#_./ _)" [0, 0, 10] 10)
"_Bleast_mset" :: "id => 'a multiset => bool => 'a" ("(3LEAST _:#_./ _)" [0, 0, 10] 10)
syntax (HOL)
"_Ball_mset" :: "pttrn => 'a multiset => bool => bool" ("(3! _:#_./ _)" [0, 0, 10] 10)
"_Bex_mset" :: "pttrn => 'a multiset => bool => bool" ("(3? _:#_./ _)" [0, 0, 10] 10)
"_Bex1_mset" :: "pttrn => 'a multiset => bool => bool" ("(3?! _:#_./ _)" [0, 0, 10] 10)
syntax
"_Ball_mset" :: "pttrn => 'a multiset => bool => bool" ("(3∀_∈#_./ _)" [0, 0, 10] 10)
"_Bex_mset" :: "pttrn => 'a multiset => bool => bool" ("(3∃_∈#_./ _)" [0, 0, 10] 10)
"_Bex1_mset" :: "pttrn => 'a multiset => bool => bool" ("(3∃!_∈#_./ _)" [0, 0, 10] 10)
"_Bleast_mset" :: "id => 'a multiset => bool => 'a" ("(3LEAST_∈#_./ _)" [0, 0, 10] 10)
syntax (HTML output)
"_Ball_mset" :: "pttrn => 'a multiset => bool => bool" ("(3∀_∈#_./ _)" [0, 0, 10] 10)
"_Bex_mset" :: "pttrn => 'a multiset => bool => bool" ("(3∃_∈#_./ _)" [0, 0, 10] 10)
"_Bex1_mset" :: "pttrn => 'a multiset => bool => bool" ("(3∃!_∈#_./ _)" [0, 0, 10] 10)
translations
"ALL x:#A. P" ⇌ "CONST Ball_mset A (%x. P)"
"EX x:#A. P" ⇌ "CONST Bex_mset A (%x. P)"
"EX! x:#A. P" ⇀ "EX! x. x:#A & P"
"LEAST x:#A. P" ⇀ "LEAST x. x:#A & P"
syntax (ASCII output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<#_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<#_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=#_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=#_./ _)" [0, 0, 10] 10)
"_setleEx1" :: "[idt, 'a, bool] => bool" ("(3EX! _<=#_./ _)" [0, 0, 10] 10)
syntax
"_setlessAll_mset" :: "[idt, 'a, bool] => bool" ("(3∀_⊂#_./ _)" [0, 0, 10] 10)
"_setlessEx_mset" :: "[idt, 'a, bool] => bool" ("(3∃_⊂#_./ _)" [0, 0, 10] 10)
"_setleAll_mset" :: "[idt, 'a, bool] => bool" ("(3∀_⊆#_./ _)" [0, 0, 10] 10)
"_setleEx_mset" :: "[idt, 'a, bool] => bool" ("(3∃_⊆#_./ _)" [0, 0, 10] 10)
"_setleEx1_mset" :: "[idt, 'a, bool] => bool" ("(3∃!_⊆#_./ _)" [0, 0, 10] 10)
syntax (HOL output)
"_setlessAll_mset" :: "[idt, 'a, bool] => bool" ("(3! _<#_./ _)" [0, 0, 10] 10)
"_setlessEx_mset" :: "[idt, 'a, bool] => bool" ("(3? _<#_./ _)" [0, 0, 10] 10)
"_setleAll_mset" :: "[idt, 'a, bool] => bool" ("(3! _<=#_./ _)" [0, 0, 10] 10)
"_setleEx_mset" :: "[idt, 'a, bool] => bool" ("(3? _<=#_./ _)" [0, 0, 10] 10)
"_setleEx1_mset" :: "[idt, 'a, bool] => bool" ("(3?! _<=#_./ _)" [0, 0, 10] 10)
syntax (HTML output)
"_setlessAll_mset" :: "[idt, 'a, bool] => bool" ("(3∀_⊂#_./ _)" [0, 0, 10] 10)
"_setlessEx_mset" :: "[idt, 'a, bool] => bool" ("(3∃_⊂#_./ _)" [0, 0, 10] 10)
"_setleAll_mset" :: "[idt, 'a, bool] => bool" ("(3∀_⊆#_./ _)" [0, 0, 10] 10)
"_setleEx_mset" :: "[idt, 'a, bool] => bool" ("(3∃_⊆#_./ _)" [0, 0, 10] 10)
"_setleEx1_mset" :: "[idt, 'a, bool] => bool" ("(3∃!_⊆#_./ _)" [0, 0, 10] 10)
translations
"∀A⊂#B. P" => "ALL A. A ⊂# B --> P"
"∃A⊂#B. P" => "EX A. A ⊂# B & P"
"∀A⊆#B. P" => "ALL A. A ⊆# B --> P"
"∃A⊆#B. P" => "EX A. A ⊆# B & P"
"∃!A⊆#B. P" => "EX! A. A ⊆# B & P"
print_translation ‹
let
val All_mset_binder = Mixfix.binder_name @{const_syntax All};
val Ex_mset_binder = Mixfix.binder_name @{const_syntax Ex};
val impl = @{const_syntax HOL.implies};
val conj = @{const_syntax HOL.conj};
val sbset = @{const_syntax subset_mset};
val sbset_eq = @{const_syntax subseteq_mset};
val trans =
[((All_mset_binder, impl, sbset), @{syntax_const "_setlessAll_mset"}),
((All_mset_binder, impl, sbset_eq), @{syntax_const "_setleAll_mset"}),
((Ex_mset_binder, conj, sbset), @{syntax_const "_setlessEx_mset"}),
((Ex_mset_binder, conj, sbset_eq), @{syntax_const "_setleEx_mset"})];
fun mk v (v', T) c n P =
if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
then Syntax.const c $ Syntax_Trans.mark_bound_body (v', T) $ n $ P
else raise Match;
fun tr' q = (q, fn _ =>
(fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name multiset}, _)),
Const (c, _) $
(Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
(case AList.lookup (op =) trans (q, c, d) of
NONE => raise Match
| SOME l => mk v (v', T) l n P)
| _ => raise Match));
in
[tr' All_mset_binder, tr' Ex_mset_binder]
end
›
print_translation ‹
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball_mset} @{syntax_const "_Ball_mset"},
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex_mset} @{syntax_const "_Bex_mset"}]
› ― ‹to avoid eta-contraction of body›
simproc_setup defined_Bex_mset ("EX x:#A. P x & Q x") = ‹
fn _ => Quantifier1.rearrange_bex
(fn ctxt =>
unfold_tac ctxt @{thms Bex_mset_def} THEN
Quantifier1.prove_one_point_ex_tac ctxt)
›
simproc_setup defined_All_mset ("ALL x:#A. P x --> Q x") = ‹
fn _ => Quantifier1.rearrange_ball
(fn ctxt =>
unfold_tac ctxt @{thms Ball_mset_def} THEN
Quantifier1.prove_one_point_all_tac ctxt)
›
lemma ball_msetI [intro!]: "(!!x. x:#A ==> P x) ==> ALL x:#A. P x"
by (simp add: Ball_mset_def)
lemma bspec_mset [dest?]: "ALL x:#A. P x ==> x:#A ==> P x"
by (simp add: Ball_mset_def)
text ‹
Gives better instantiation for bound:
›
setup ‹
map_theory_claset (fn ctxt =>
ctxt addbefore ("bspec_mset", fn ctxt' => dresolve_tac ctxt' @{thms bspec_mset}
THEN' assume_tac ctxt'))
›
ML ‹
structure Simpdata =
struct
open Simpdata;
val mksimps_pairs_mset = [(@{const_name Ball_mset}, @{thms bspec_mset})] @ mksimps_pairs;
end;
open Simpdata;
›
declaration ‹fn _ =>
Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs_mset))
›
lemma ball_msetE [elim]: "ALL x:#A. P x ==> (P x ==> Q) ==> (x ~:# A ==> Q) ==> Q"
by (unfold Ball_mset_def) blast
lemma bex_msetI [intro]: "P x ==> x:#A ==> EX x:#A. P x"
― ‹Normally the best argument order: @{prop "P x"} constrains the
choice of @{prop "x:#A"}.›
by (unfold Bex_mset_def) blast
lemma rev_bex_msetI [intro]: "x:#A ==> P x ==> EX x:#A. P x"
― ‹The best argument order when there is only one @{prop "x:#A"}.›
by (unfold Bex_mset_def) blast
lemma bex_msetCI: "(ALL x:#A. ~P x ==> P a) ==> a:#A ==> EX x:#A. P x"
by (unfold Bex_mset_def) blast
lemma bex_msetE [elim!]: "EX x:#A. P x ==> (!!x. x:#A ==> P x ==> Q) ==> Q"
by (unfold Bex_mset_def) blast
lemma ball_mset_triv [simp]: "(ALL x:#A. P) = ((EX x. x:#A) --> P)"
― ‹Trival rewrite rule.›
by (simp add: Ball_mset_def)
lemma bex_mset_triv [simp]: "(EX x:#A. P) = ((EX x. x:#A) & P)"
― ‹Dual form for existentials.›
by (simp add: Bex_mset_def)
lemma bex_mset_triv_one_point1 [simp]: "(EX x:#A. x = a) = (a:#A)"
by blast
lemma bex_mset_triv_one_point2 [simp]: "(EX x:#A. a = x) = (a:#A)"
by blast
lemma bex_mset_one_point1 [simp]: "(EX x:#A. x = a & P x) = (a:#A & P a)"
by blast
lemma bex_mset_one_point2 [simp]: "(EX x:#A. a = x & P x) = (a:#A & P a)"
by blast
lemma ball_mset_one_point1 [simp]: "(ALL x:#A. x = a --> P x) = (a:#A --> P a)"
by blast
lemma ball_mset_one_point2 [simp]: "(ALL x:#A. a = x --> P x) = (a:#A --> P a)"
by blast
lemma ball_mset_conj_distrib:
"(∀x∈#A. P x ∧ Q x) ⟷ ((∀x∈#A. P x) ∧ (∀x∈#A. Q x))"
by blast
lemma bex_disj_distrib:
"(∃x∈#A. P x ∨ Q x) ⟷ ((∃x∈#A. P x) ∨ (∃x∈#A. Q x))"
by blast
text ‹Congruence rules›
lemma ball_mset_cong:
"A = B ==> (!!x. x:#B ==> P x = Q x) ==>
(ALL x:#A. P x) = (ALL x:#B. Q x)"
by (simp add: Ball_mset_def)
lemma strong_ball_mset_cong [cong]:
"A = B ==> (!!x. x:#B =simp=> P x = Q x) ==>
(ALL x:#A. P x) = (ALL x:#B. Q x)"
by (simp add: simp_implies_def Ball_mset_def)
lemma bex_mset_cong:
"A = B ==> (!!x. x:#B ==> P x = Q x) ==>
(EX x:#A. P x) = (EX x:#B. Q x)"
by (simp add: Bex_mset_def cong: conj_cong)
lemma strong_bex_mset_cong [cong]:
"A = B ⟹ (!!x. x:#B =simp=> P x = Q x) ==>
(EX x:#A. P x) = (EX x:#B. Q x)"
by (simp add: simp_implies_def Bex_mset_def cong: conj_cong)
lemma bex1_mset_def: "(∃!x∈#X. P x) ⟷ (∃x∈#X. P x) ∧ (∀x∈#X. ∀y∈#X. P x ⟶ P y ⟶ x = y)"
by auto
text ‹More: this rules are here to help the simplifier›
lemma Bex_mset_singleton[iff]: "(∃L∈#{#a#}. P L) ⟷ P a"
by (auto split: split_if_asm)
lemma Ball_mset_singleton[iff]: "(∀L∈#{#a#}. P L) ⟷ P a"
by (auto split: split_if_asm)
lemma Bex_mset_mempty[iff]: "(∃L∈#{#}. P L) ⟷ False"
by (auto simp add: Bex_mset_def)
lemma Ball_mset_mempty[iff]: "(∀L∈#{#}. P L) ⟷ True"
by (auto simp add: Bex_mset_def)
subsection ‹Lemmas about intersection›
lemma mset_inter_single:
"x ∈# Σ ⟹ Σ #∩ {#x#} = {#x#}"
"x ∉# Σ ⟹ Σ #∩ {#x#} = {#}"
apply (simp add: mset_le_single subset_mset.inf_absorb2)
by (simp add: multiset_inter_def)
subsection ‹Lemmas about cardinality›
text ‹
This sections adds various lemmas about size. Most lemmas have a finite set equivalent.
›
lemma size_Suc_Diff1:
"x ∈# Σ ⟹ Suc (size (Σ - {#x#})) = size Σ"
using arg_cong[OF insert_DiffM, of _ _ size] by simp
lemma size_Diff_singleton: "x ∈# Σ ⟹ size (Σ - {#x#}) = size Σ - 1"
by (simp add: size_Suc_Diff1 [symmetric])
lemma size_Diff_singleton_if: "size (A - {#x#}) = (if x ∈# A then size A - 1 else size A)"
by (simp add: size_Diff_singleton)
lemma size_Un_Int:
"size A + size B = size (A #∪ B) + size (A #∩ B)"
proof -
have *: "A + B = B + (A - B + (A - (A - B)))"
by (simp add: subset_mset.add_diff_inverse union_commute)
have "size B + size (A - B) = size A + size (B - A)"
unfolding size_union[symmetric] subset_mset.sup_commute sup_subset_mset_def[symmetric]
by blast
then show ?thesis unfolding multiset_inter_def size_union[symmetric] "*"
by (auto simp add: sup_subset_mset_def)
qed
lemma size_Un_disjoint:
assumes "A #∩ B = {#}"
shows "size (A #∪ B) = size A + size B"
using assms size_Un_Int [of A B] by simp
lemma size_Diff_subset_Int:
shows "size (Σ - Σ') = size Σ - size (Σ #∩ Σ')"
proof -
have "Σ - Σ' = Σ - Σ #∩ Σ'" by (auto simp add: multiset_eq_iff)
thus ?thesis by (simp add: size_Diff_submset)
qed
lemma diff_size_le_size_Diff: "size (Σ:: _ multiset) - size Σ' ≤ size (Σ - Σ')"
proof-
have "size Σ - size Σ' ≤ size Σ - size (Σ #∩ Σ')"
using size_mset_mono diff_le_mono2 subset_mset.inf_le2 by blast
also have "… = size(Σ-Σ')" using assms by(simp add: size_Diff_subset_Int)
finally show ?thesis .
qed
lemma size_Diff1_less: "x∈# Σ ⟹ size (Σ - {#x#}) < size Σ"
apply (rule Suc_less_SucD)
by (simp add: size_Suc_Diff1)
lemma size_Diff2_less: "x∈# Σ ⟹ y∈# Σ ⟹ size (Σ - {#x#} - {#y#}) < size Σ"
using nonempty_has_size by (fastforce intro!: diff_Suc_less simp add: size_Diff1_less
size_Diff_subset_Int mset_inter_single)
lemma size_Diff1_le: "size (Σ - {#x#}) ≤ size Σ"
by (cases "x ∈# Σ") (simp_all add: size_Diff1_less less_imp_le)
lemma size_psubset: "(Σ:: _ multiset) ≤# Σ' ⟹ size Σ < size Σ' ⟹ Σ <# Σ'"
using less_irrefl subset_mset_def by blast
subsection ‹Multiset Extension of Multiset Ordering›
text ‹
The ‹op #⊂##› and ‹op #⊆##› operators are introduced as the multiset extension of
the multiset orderings of @{term "op #⊂#"} and @{term "op #⊆#"}.
›
definition less_mset_mset :: "('a :: order) multiset multiset ⇒ 'a multiset multiset ⇒ bool"
(infix "#<##" 50)
where
"M' #<## M ⟷ (M', M) ∈ mult {(x', x). x' #<# x}"
definition le_mset_mset :: "('a :: order) multiset multiset ⇒ 'a multiset multiset ⇒ bool"
(infix "#<=##" 50)
where
"M' #<=## M ⟷ M' #<## M ∨ M' = M"
notation less_mset_mset (infix "#⊂##" 50)
notation le_mset_mset (infix "#⊆##" 50)
lemmas less_mset_mset⇩D⇩M = order.mult⇩D⇩M[OF order_multiset, folded less_mset_mset_def]
lemmas less_mset_mset⇩H⇩O = order.mult⇩H⇩O[OF order_multiset, folded less_mset_mset_def]
interpretation multiset_multiset_order: order
"le_mset_mset :: ('a :: linorder) multiset multiset ⇒ ('a :: linorder) multiset multiset ⇒ bool"
"less_mset_mset :: ('a :: linorder) multiset multiset ⇒ ('a::linorder) multiset multiset ⇒ bool"
unfolding less_mset_mset_def[abs_def] le_mset_mset_def[abs_def] less_multiset_def[abs_def]
by (rule order.order_mult)+ standard
interpretation multiset_multiset_linorder: linorder
"le_mset_mset :: ('a :: linorder) multiset multiset ⇒ ('a :: linorder) multiset multiset ⇒ bool"
"less_mset_mset :: ('a :: linorder) multiset multiset ⇒ ('a::linorder) multiset multiset ⇒ bool"
unfolding less_mset_mset_def[abs_def] le_mset_mset_def[abs_def]
by (rule linorder.linorder_mult[OF linorder_multiset])
lemma wf_less_mset_mset: "wf {(Σ :: ('a :: wellorder) multiset multiset, T). Σ #⊂## T}"
unfolding less_mset_mset_def by (auto intro: wf_mult wf_less_multiset)
interpretation multiset_multiset_wellorder: wellorder
"le_mset_mset :: ('a::wellorder) multiset multiset ⇒ ('a::wellorder) multiset multiset ⇒ bool"
"less_mset_mset :: ('a::wellorder) multiset multiset ⇒ ('a::wellorder) multiset multiset ⇒ bool"
by unfold_locales (blast intro: wf_less_mset_mset[unfolded wf_def, rule_format])
lemma union_less_mset_mset_mono2: "B #⊂## D ⟹ C + B #⊂## C + (D::'a::order multiset multiset)"
apply (unfold less_mset_mset_def mult_def)
apply (erule trancl_induct)
apply (blast intro: mult1_union)
apply (blast intro: mult1_union trancl_trans)
done
lemma union_less_mset_mset_diff_plus:
"U ≤# Σ ⟹ T #⊂## U ⟹ Σ - U + T #⊂## Σ"
apply (drule subset_mset.diff_add[symmetric])
using union_less_mset_mset_mono2[of T U "Σ - U"] by simp
lemma ex_gt_imp_less_mset_mset:
"(∃y :: 'a :: linorder multiset ∈# T. (∀x. x ∈# Σ ⟶ x #⊂# y)) ⟹ Σ #⊂## T"
using less_mset_mset⇩H⇩O by force
subsection ‹Multiset and set conversion›
lemma mset_set_set_mset_empty_mempty[iff]:
"mset_set (set_mset D) = {#} ⟷ D = {#}"
by (auto dest: arg_cong[of _ _ set_mset])
lemma count_mset_0[iff]: "count (mset D) L = 0 ⟷ L ∉ set D"
by (metis in_multiset_in_set not_gr0)
lemma count_mset_set_le_1[simp]: "count (mset_set (set C)) L ≤ 1"
by (metis List.finite_set One_nat_def count_mset_set(1) count_mset_set(3) le_less_linear
less_nat_zero_code less_not_refl)
lemma replicate_mset_plus: "replicate_mset (a + b) C = replicate_mset a C + replicate_mset b C"
by (induct a) (auto simp: ac_simps)
lemma set_mset_minus_replicate_mset:
"n ≥ count A a ⟹ set_mset (A - replicate_mset n a) = set_mset A - {a}"
"n < count A a ⟹ set_mset (A - replicate_mset n a) = set_mset A"
by (auto split: split_if_asm)
abbreviation remove_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" where
"remove_mset C M ≡ M - replicate_mset (count M C) C"
lemma mset_removeAll[simp]:
"mset (removeAll C L) = remove_mset C (mset L)"
by (induction L) (auto simp: ac_simps multiset_eq_iff)
lemma set_mset_single_iff_replicate_mset:
"set_mset U = {a} ⟷ (∃n>0. U = replicate_mset n a)"
apply (rule iffI)
apply (metis antisym_conv3 count_replicate_mset gr_implies_not0 mem_set_mset_iff multiset_eq_iff
singleton_iff)
by (auto split: split_if_asm)
lemma count_mset_set_le_one: "count (mset_set A) x ≤ 1"
by (metis count_mset_set(1) elem_mset_set le_less less_eq_nat.simps(1) mset_set.infinite
zero_multiset.rep_eq)
lemma mset_set_subseteq_mset_set[iff]:
assumes "finite A" "finite B"
shows "mset_set A ⊆# mset_set B ⟷ A ⊆ B"
proof -
{ assume "¬ mset_set A ⊆# mset_set B"
have "mset_set A ⊆# mset_set B ∨ (∃a. a ∉ B ∧ a ∈ A)"
using assms(2) by (metis count_mset_set(1) count_mset_set(3) count_mset_set_le_one
elem_mset_set le_less_linear mset_less_eqI)
then have "A ⊆ B ⟶ mset_set A ⊆# mset_set B"
by (meson contra_subsetD) }
then show ?thesis
using assms by (metis (full_types) finite_set_mset_mset_set set_mset_mono)
qed
lemma mset_set_set_mset_subseteq[simp]: "mset_set (set_mset A) ⊆# A"
by (metis count_mset_set(1) count_mset_set(3) finite_set_mset le_less_linear less_one
mem_set_mset_iff mset_less_eqI not_gr0)
lemma mset_sorted_list_of_set[simp]:
"mset (sorted_list_of_set A) = mset_set A"
by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set)
lemma mset_take_subseteq: "mset (take n xs) ⊆# mset xs"
apply (induct xs arbitrary: n)
apply simp
by (case_tac n) simp_all
subsection ‹Removing duplicates›
definition remdups_mset :: "'v multiset ⇒ 'v multiset" where
"remdups_mset S = mset_set (set_mset S)"
lemma remdups_mset_in[iff]: "a ∈# remdups_mset A ⟷ a ∈# A"
unfolding remdups_mset_def by auto
lemma count_remdups_mset_eq_1: "a ∈# remdups_mset A ⟷ count (remdups_mset A) a = 1"
unfolding remdups_mset_def by fastforce
lemma remdups_mset_empty[simp]:
"remdups_mset {#} = {#}"
unfolding remdups_mset_def by auto
lemma remdups_mset_singleton[simp]:
"remdups_mset {#a#} = {#a#}"
unfolding remdups_mset_def by auto
lemma set_mset_remdups[simp]: "set_mset (remdups_mset C) = set_mset C"
by auto
lemma remdups_mset_eq_empty[iff]:
"remdups_mset D = {#} ⟷ D = {#}"
unfolding remdups_mset_def by blast
lemma remdups_mset_singleton_sum[simp]:
"remdups_mset ({#a#} + A) = (if a ∈# A then remdups_mset A else {#a#} + remdups_mset A)"
"remdups_mset (A+{#a#}) = (if a ∈# A then remdups_mset A else {#a#} + remdups_mset A)"
unfolding remdups_mset_def by (simp_all add: insert_absorb)
lemma mset_remdups_remdups_mset[simp]:
"mset (remdups D) = remdups_mset (mset D)"
by (induction D) (auto simp add: ac_simps)
definition distinct_mset :: "'a multiset ⇒ bool" where
"distinct_mset S ⟷ (∀a. a ∈# S ⟶ count S a = 1)"
lemma distinct_mset_empty[simp]: "distinct_mset {#}"
unfolding distinct_mset_def by auto
lemma distinct_mset_singleton[simp]: "distinct_mset {#a#}"
unfolding distinct_mset_def by auto
definition distinct_mset_set :: "'a multiset set ⇒ bool" where
"distinct_mset_set Σ ⟷ (∀S ∈Σ. distinct_mset S)"
lemma distinct_mset_set_empty[simp]:
"distinct_mset_set {}"
unfolding distinct_mset_set_def by auto
lemma distinct_mset_set_singleton[iff]:
"distinct_mset_set {A} ⟷ distinct_mset A"
unfolding distinct_mset_set_def by auto
lemma distinct_mset_set_insert[iff]:
"distinct_mset_set (insert S Σ) ⟷ (distinct_mset S ∧ distinct_mset_set Σ)"
unfolding distinct_mset_set_def by auto
lemma distinct_mset_set_union[iff]:
"distinct_mset_set (Σ ∪ Σ') ⟷ (distinct_mset_set Σ ∧ distinct_mset_set Σ')"
unfolding distinct_mset_set_def by auto
lemma distinct_mset_union:
"distinct_mset (A + B) ⟹ distinct_mset A"
by (simp add: add_is_1 distinct_mset_def)
lemma distinct_mset_minus[simp]:
"distinct_mset A ⟹ distinct_mset (A - B)"
by (metis Multiset.diff_le_self mset_le_exists_conv distinct_mset_union)
lemma in_distinct_mset_set_distinct_mset:
"a ∈ Σ ⟹ distinct_mset_set Σ ⟹ distinct_mset a"
unfolding distinct_mset_set_def by auto
lemma distinct_mset_remdups_mset[simp]: "distinct_mset (remdups_mset S)"
using count_remdups_mset_eq_1 unfolding distinct_mset_def by metis
lemma distinct_mset_distinct[simp]:
"distinct_mset (mset x) = distinct x"
unfolding distinct_mset_def
by (induction x) (simp_all add: distinct_count_atmost_1)
lemma count_mset_set_if:
"count (mset_set A) a = (if a ∈ A ∧ finite A then 1 else 0)"
by auto
lemma distinct_mset_rempdups_union_mset:
assumes "distinct_mset A" and "distinct_mset B"
shows "A #∪ B = remdups_mset (A + B)"
using assms unfolding remdups_mset_def
using le_less by (fastforce simp: multiset_eq_iff max_def count_mset_set_if distinct_mset_def)
lemma distinct_mset_set_distinct:
"distinct_mset_set (mset ` set Cs) ⟷ (∀c∈ set Cs. distinct c)"
unfolding distinct_mset_set_def by auto
lemma distinct_mset_add_single:
"distinct_mset ({#a#} + L) ⟷ distinct_mset L ∧ a ∉# L"
unfolding distinct_mset_def
apply (rule iffI)
prefer 2 apply auto[]
apply standard
apply (intro allI)
apply (rename_tac aa)
apply (case_tac "a = aa")
by (auto split: split_if_asm)
lemma distinct_mset_single_add:
"distinct_mset (L + {#a#}) ⟷ distinct_mset L ∧ a ∉# L"
using add.commute[of L "{#a#}"] distinct_mset_add_single by force
lemma distinct_mset_size_eq_card:
"distinct_mset C ⟹ size C = card (set_mset C)"
by (induction C) (auto simp: distinct_mset_single_add)
text ‹Another characterisation of @{term distinct_mset}›
lemma distinct_mset_count_less_1:
"distinct_mset S ⟷ (∀a. count S a ≤ 1)"
unfolding distinct_mset_def by (metis le_neq_implies_less less_one less_or_eq_imp_le not_gr0)
lemma distinct_mset_add:
"distinct_mset (L + L') ⟷ distinct_mset L ∧ distinct_mset L' ∧ L #∩ L' = {#}" (is "?A ⟷ ?B")
proof (rule iffI)
assume ?A
have L: "distinct_mset L"
using ‹distinct_mset (L + L')› distinct_mset_union by blast
moreover have L': "distinct_mset L'"
using ‹distinct_mset (L + L')› distinct_mset_union unfolding add.commute[of L L'] by blast
moreover have "L #∩ L' = {#}"
using L L' unfolding multiset_inter_def multiset_eq_iff by (metis Nat.diff_le_self
‹distinct_mset (L + L')› add_diff_cancel_left' count_diff count_empty
diff_is_0_eq distinct_mset_count_less_1 eq_iff le_neq_implies_less less_one)
ultimately show ?B by fast
next
assume ?B
show ?A
unfolding distinct_mset_count_less_1
proof (intro allI)
fix a
have "count (L + L') a ≤ count L a + count L' a"
by auto
moreover have "count L a + count L' a ≤ 1"
using ‹?B› by (metis One_nat_def add_eq_if add_is_1 distinct_mset_def empty_inter le_Suc_eq
mset_inter_single(1) not_gr0 single_not_empty subset_mset.inf_assoc zero_le_one)
ultimately show "count (L + L') a ≤ 1"
by arith
qed
qed
lemma distinct_mset_set_mset_ident[simp]: "distinct_mset M ⟹ mset_set (set_mset M) = M"
apply (auto simp: multiset_eq_iff)
apply (rename_tac x)
apply (case_tac "count M x = 0")
apply simp
apply (case_tac "count M x = 1")
apply simp
unfolding distinct_mset_count_less_1
by (meson le_neq_implies_less less_one)
lemma distinct_finite_set_mset_subseteq_iff[iff]:
assumes dist: "distinct_mset M" and fin: "finite N"
shows "set_mset M ⊆ N ⟷ M ⊆# mset_set N"
proof
assume "set_mset M ⊆ N"
then show "M ⊆# mset_set N"
by (metis dist distinct_mset_set_mset_ident fin finite_subset mset_set_subseteq_mset_set)
next
assume "M ⊆# mset_set N"
then show "set_mset M ⊆ N"
by (metis contra_subsetD empty_iff finite_set_mset_mset_set infinite_set_mset_mset_set
set_mset_mono subsetI)
qed
lemma distinct_mem_diff_mset:
assumes dist: "distinct_mset M" and mem: "x ∈ set_mset (M - N)"
shows "x ∉ set_mset N"
proof -
have "count M x = 1"
using dist mem by (simp add: distinct_mset_def)
then show ?thesis
using mem by simp
qed
lemma distinct_set_mset_eq:
assumes
dist_m: "distinct_mset M" and
dist_n: "distinct_mset N" and
set_eq: "set_mset M = set_mset N"
shows "M = N"
proof -
have "mset_set (set_mset M) = mset_set (set_mset N)"
using set_eq by simp
thus ?thesis
using dist_m dist_n by auto
qed
lemma distinct_mset_union_mset:
assumes
"distinct_mset D" and
"distinct_mset C"
shows "distinct_mset (D #∪ C)"
using assms unfolding distinct_mset_count_less_1 by force
lemma distinct_mset_inter_mset:
assumes
"distinct_mset D" and
"distinct_mset C"
shows "distinct_mset (D #∩ C)"
using assms unfolding distinct_mset_count_less_1
by (meson dual_order.trans subset_mset.inf_le2 subseteq_mset_def)
subsection ‹Filter›
lemma mset_filter_compl: "mset (filter p xs) + mset (filter (Not ∘ p) xs) = mset xs"
apply (induct xs)
by simp
(metis (no_types) add_diff_cancel_left' comp_apply filter.simps(2) mset.simps(2)
mset_compl_union)
lemma singleton_subseteq_iff[iff]: "{#x#} ⊆# A ⟷ x ∈# A"
by (meson mset_leD mset_le_single multi_member_last)
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_filter_ne_mset[simp]:
"image_mset f {#x ∈# M. f x ≠ y#} = remove_mset y (image_mset f M)"
by (induct M, auto, meson count_le_replicate_mset_le order_refl subset_mset.add_diff_assoc2)
lemma comprehension_mset_False[simp]:
"{# L ∈# A. False#} = {#}"
by (auto simp: multiset_eq_iff)
lemma filter_mset_eq:
"filter_mset (op = L) A = replicate_mset (count A L) L"
by (auto simp: multiset_eq_iff)
subsection ‹Sums›
lemma msetsum_distrib[simp]:
fixes C D :: "'a ⇒ 'b::{comm_monoid_add}"
shows "(∑x∈#A. C x + D x) = (∑x∈#A. C x) + (∑x∈#A. D x)"
by (induction A) (auto simp: ac_simps)
lemma msetsum_union_disjoint:
assumes "A #∩ B = {#}"
shows "(∑La∈#A #∪ B. f La) =
(∑La∈#A. f La) + (∑La∈#B. f La)"
by (metis assms diff_zero empty_sup image_mset_union msetsum.union multiset_inter_commute
multiset_union_diff_commute sup_subset_mset_def zero_diff)
subsection ‹Order›
text ‹Instantiating multiset order as a linear order.
TODO: remove when multiset is of sort ord again›
instantiation multiset :: (linorder) linorder
begin
definition less_multiset :: "'a::linorder multiset ⇒ 'a multiset ⇒ bool" where
"M' < M ⟷ M' #⊂# M"
definition less_eq_multiset :: "'a multiset ⇒ 'a multiset ⇒bool" where
"(M'::'a multiset) ≤ M ⟷ M' #⊆# M"
instance
by standard (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le
add.commute multiset_order.add_right_mono)
end
end