Theory PAPP_Multiset_Extras

(*
  File:     PAPP_Multiset_Extras.thy
  Author:   Manuel Eberl, University of Innsbruck 
*)
section ‹Auxiliary Facts About Multisets›
theory PAPP_Multiset_Extras
  imports "HOL-Library.Multiset"
begin

text ‹
  This section contains a number of not particularly interesting small facts about multisets.
›

lemma mset_set_subset_iff: "finite A ⟹ mset_set A ⊆# B ⟷ A ⊆ set_mset B"
  by (metis finite_set_mset finite_set_mset_mset_set mset_set_set_mset_msubset 
            msubset_mset_set_iff set_mset_mono subset_mset.trans)

lemma mset_subset_size_ge_imp_eq:
  assumes "A ⊆# B" "size A ≥ size B"
  shows   "A = B"
  using assms
proof (induction A arbitrary: B)
  case empty
  thus ?case by auto
next
  case (add x A B)
  have [simp]: "x ∈# B"
    using add.prems  by (simp add: insert_subset_eq_iff)
  define B' where "B' = B - {#x#}"
  have B_eq: "B = add_mset x B'"
    using add.prems unfolding B'_def by (auto simp: add_mset_remove_trivial_If)
  have "A = B'"
    using add.prems by (intro add.IH) (auto simp: B_eq)
  thus ?case
    by (auto simp: B_eq)
qed

lemma mset_psubset_iff:
  "X ⊂# Y ⟷ X ⊆# Y ∧ (∃x. count X x < count Y x)"
  by (meson less_le_not_le subset_mset.less_le_not_le subseteq_mset_def)
  
lemma count_le_size: "count A x ≤ size A"
  by (induction A) auto

lemma size_filter_eq_conv_count [simp]: "size (filter_mset (λy. y = x) A) = count A x"
  by (induction A) auto

lemma multiset_filter_mono':
  assumes "⋀x. x ∈# A ⟹ P x ⟹ Q x"
  shows   "filter_mset P A ⊆# filter_mset Q A"
  using assms by (induction A)  (auto simp: subset_mset.absorb_iff1 add_mset_union)

lemma multiset_filter_mono'':
  assumes "A ⊆# B" "⋀x. x ∈# A ⟹ P x ⟹ Q x"
  shows "filter_mset P A ⊆# filter_mset Q B"
  using assms multiset_filter_mono multiset_filter_mono'
  by (metis subset_mset.order_trans)

lemma filter_mset_disjunction:
  assumes "⋀x. x ∈# X ⟹ P x ⟹ Q x ⟹ False"
  shows   "filter_mset (λx. P x ∨ Q x) X = filter_mset P X + filter_mset Q X"
  using assms by (induction X) auto
  
lemma size_mset_sum_mset: "size (sum_mset X) = (∑x∈#X. size (x :: 'a multiset))"
  by (induction X) auto

lemma count_sum_mset: "count (sum_mset X) x = (∑Y∈#X. count Y x)"
  by (induction X) auto

lemma replicate_mset_rec: "n > 0 ⟹ replicate_mset n x = add_mset x (replicate_mset (n - 1) x)"
  by (cases n) auto

lemma add_mset_neq: "x ∉# B ⟹ add_mset x A ≠ B"
  by force

lemma filter_replicate_mset:
  "filter_mset P (replicate_mset n x) = (if P x then replicate_mset n x else {#})"
  by (induction n) auto

lemma filter_diff_mset': "filter_mset P (X - Y) = filter_mset P X - Y"
  by (rule multiset_eqI) auto

lemma in_diff_multiset_absorb2: "x ∉# B ⟹ x ∈# A - B ⟷ x ∈# A"
  by (metis count_greater_zero_iff count_inI in_diff_count)

end