Theory Card_Multisets.Card_Multisets

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Cardinality of Multisets›

theory Card_Multisets
imports
  "HOL-Library.Multiset"
begin

subsection ‹Additions to Multiset Theory›

lemma mset_set_set_mset_subseteq:
  "mset_set (set_mset M) ⊆# M"
proof (induct M)
  case empty
  show ?case by simp
next
  case (add x M)
  from this show ?case
  proof (cases "x ∈# M")
    assume "x ∈# M"
    from this have "mset_set (set_mset (M + {#x#})) = mset_set (set_mset M)"
      by (simp add: insert_absorb)
    from this add.hyps show ?thesis
      using subset_mset.trans by fastforce
  next
    assume "¬ x ∈# M"
    from this add.hyps have "{#x#} + mset_set (set_mset M) ⊆# M + {#x#}"
      by (simp add: insert_subset_eq_iff)
    from this ‹¬ x ∈# M› show ?thesis by simp
  qed
qed

lemma size_mset_set_eq_card:
  assumes "finite A"
  shows "size (mset_set A) = card A"
using assms by (induct A) auto

lemma card_set_mset_leq:
  "card (set_mset M) ≤ size M"
by (induct M) (auto simp add: card_insert_le_m1)

subsection ‹Lemma to Enumerate Sets of Multisets›

lemma set_of_multisets_eq:
  assumes "x ∉ A"
  shows "{M. set_mset M ⊆ insert x A ∧ size M = Suc k} =
    {M. set_mset M ⊆ A ∧ size M = Suc k} ∪
    (λM. M + {#x#}) ` {M. set_mset M ⊆ insert x A ∧ size M = k}"
proof -
  from ‹x ∉ A› have "{M. set_mset M ⊆ insert x A ∧ size M = Suc k} =
    {M. set_mset M ⊆ A ∧ size M = Suc k} ∪
    {M. set_mset M ⊆ insert x A ∧ size M = Suc k ∧ x ∈# M}"
    by auto
  moreover have "{M. set_mset M ⊆ insert x A ∧ size M = Suc k ∧ x ∈# M} =
    (λM. M + {#x#}) ` {M. set_mset M ⊆ insert x A ∧ size M = k}" (is "?S = ?T")
  proof
    show "?S ⊆ ?T"
    proof
      fix M
      assume "M ∈ ?S"
      from this have "M = M - {#x#} + {#x#}" by auto
      moreover have "M - {#x#} ∈ {M. set_mset M ⊆ insert x A ∧ size M = k}"
      proof -
        have "set_mset (M - {#x#} + {#x#}) ⊆ insert x A"
          using ‹M ∈ ?S› by force
        moreover have "size (M - {#x#} + {#x#}) = Suc k ∧ x ∈# M - {#x#} + {#x#}"
          using ‹M ∈ ?S› by force
        ultimately show ?thesis by force
      qed
      ultimately show "M ∈ ?T" by auto
    qed
  next
    show "?T ⊆ ?S" by force
  qed
  ultimately show ?thesis by auto
qed

subsection ‹Derivation of Suitable Induction Rule›

context
begin

private inductive R :: "'a set ⇒ nat ⇒ bool"
where
  "finite A ⟹ R A 0"
| "R {} k"
| "finite A ⟹ x ∉ A ⟹ R A (Suc k) ⟹ R (insert x A) k ⟹ R (insert x A) (Suc k)"

private lemma R_eq_finite:
  "R A k ⟷ finite A"
proof
  assume "R A k"
  from this show "finite A" by cases auto
next
  assume "finite A"
  from this show "R A k"
  proof (induct A)
    case empty
    from this show ?case by (rule R.intros(2))
  next
    case insert
    from this show ?case
    proof (induct k)
      case 0
      from this show ?case
        by (intro R.intros(1) finite.insertI)
    next
      case Suc
      from this show ?case
        by (metis R.simps Zero_neq_Suc diff_Suc_1)
    qed
  qed
qed

lemma finite_set_and_nat_induct[consumes 1, case_names zero empty step]:
  assumes "finite A"
  assumes "⋀A. finite A ⟹ P A 0"
  assumes "⋀k. P {} k"
  assumes "⋀A k x. finite A ⟹ x ∉ A ⟹ P A (Suc k) ⟹ P (insert x A) k ⟹ P (insert x A) (Suc k)"
  shows "P A k"
proof -
  from ‹finite A› have "R A k" by (subst R_eq_finite)
  from this assms(2-4) show ?thesis by (induct A k) auto
qed

end

subsection ‹Finiteness of Sets of Multisets›

lemma finite_multisets:
  assumes "finite A"
  shows "finite {M. set_mset M ⊆ A ∧ size M = k}"
using assms
proof (induct A k rule: finite_set_and_nat_induct)
  case zero
  from this show ?case by auto
next
  case empty
  from this show ?case by auto
next
  case (step A k x)
  from this show ?case
    using set_of_multisets_eq[OF ‹x ∉ A›] by simp
qed

subsection ‹Cardinality of Multisets›

lemma card_multisets:
  assumes "finite A"
  shows "card {M. set_mset M ⊆ A ∧ size M = k} = (card A + k - 1) choose k"
using assms
proof (induct A k rule: finite_set_and_nat_induct)
  case (zero A)
  assume "finite (A :: 'a set)"
  have "{M. set_mset M ⊆ A ∧ size M = 0} = {{#}}" by auto
  from this show "card {M. set_mset M ⊆ A ∧ size M = 0} = card A + 0 - 1 choose 0"
    by simp
next
  case (empty k)
  show "card {M. set_mset M ⊆ {} ∧ size M = k} = card {} + k - 1 choose k"
    by (cases k) (auto simp add: binomial_eq_0)
next
  case (step A k x)
  let ?S⇩1 = "{M. set_mset M ⊆ A ∧ size M = Suc k}"
  and ?S⇩2 = "{M. set_mset M ⊆ insert x A ∧ size M = k}"
  assume hyps1: "card ?S⇩1 = card A + Suc k - 1 choose Suc k"
  assume hyps2: "card ?S⇩2 = card (insert x A) + k - 1 choose k"
  have finite_sets: "finite ?S⇩1" "finite ((λM. M + {#x#}) ` ?S⇩2)"
    using ‹finite A› by (auto simp add: finite_multisets)
  have inj: "inj_on (λM. M + {#x#}) ?S⇩2" by (rule inj_onI) auto
  have "card {M. set_mset M ⊆ insert x A ∧ size M = Suc k} =
    card (?S⇩1 ∪ (λM. M + {#x#}) ` ?S⇩2)"
    using set_of_multisets_eq ‹x ∉ A› by fastforce
  also have "… = card ?S⇩1 + card ((λM. M + {#x#}) ` ?S⇩2)"
    using finite_sets ‹x ∉ A› by (subst card_Un_disjoint) auto
  also have "… = card ?S⇩1 + card ?S⇩2"
    using inj by (auto intro: card_image)
  also have "… = (card A + Suc k - 1 choose Suc k) + (card (insert x A) + k - 1 choose k)"
    using hyps1 hyps2 by simp
  also have "… = card (insert x A) + Suc k - 1 choose Suc k"
    using ‹x ∉ A› ‹finite A› by simp
  finally show ?case .
qed

lemma card_too_small_multisets_covering_set:
  assumes "finite A"
  assumes "k < card A"
  shows "card {M. set_mset M = A ∧ size M = k} = 0"
proof -
  from ‹k < card A› have eq: "{M. set_mset M = A ∧ size M = k} = {}"
    using card_set_mset_leq Collect_empty_eq leD by auto
  from this show ?thesis by (metis card.empty)
qed

lemma card_multisets_covering_set:
  assumes "finite A"
  assumes "card A ≤ k"
  shows "card {M. set_mset M = A ∧ size M = k} = (k - 1) choose (k - card A)"
proof -
  have "{M. set_mset M = A ∧ size M = k} = (λM. M + mset_set A) `
    {M. set_mset M ⊆ A ∧ size M = k - card A}" (is "?S = ?f ` ?T")
  proof
    show "?S ⊆ ?f ` ?T"
    proof
      fix M
      assume "M ∈ ?S"
      from this have "M = M - mset_set A + mset_set A"
        by (auto simp add: mset_set_set_mset_subseteq subset_mset.diff_add)
      moreover from ‹M ∈ ?S› have "M - mset_set A ∈ ?T"
        by (auto simp add: mset_set_set_mset_subseteq size_Diff_submset size_mset_set_eq_card in_diffD)
      ultimately show "M ∈ ?f ` ?T" by auto
    qed
  next
    from ‹finite A› ‹card A ≤ k› show "?f ` ?T ⊆ ?S"
      by (auto simp add: size_mset_set_eq_card)+
  qed
  moreover have "inj_on ?f ?T" by (rule inj_onI) auto
  ultimately have "card ?S = card ?T" by (simp add: card_image)
  also have "… = card A + (k - card A) - 1 choose (k - card A)"
    using ‹finite A› by (simp only: card_multisets)
  also have "… = (k - 1) choose (k - card A)"
    using ‹card A ≤ k› by auto
  finally show ?thesis .
qed

end