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 ?S1 = "{M. set_mset M  A  size M = Suc k}"
  and ?S2 = "{M. set_mset M  insert x A  size M = k}"
  assume hyps1: "card ?S1 = card A + Suc k - 1 choose Suc k"
  assume hyps2: "card ?S2 = card (insert x A) + k - 1 choose k"
  have finite_sets: "finite ?S1" "finite ((λM. M + {#x#}) ` ?S2)"
    using finite A by (auto simp add: finite_multisets)
  have inj: "inj_on (λM. M + {#x#}) ?S2" by (rule inj_onI) auto
  have "card {M. set_mset M  insert x A  size M = Suc k} =
    card (?S1  (λM. M + {#x#}) ` ?S2)"
    using set_of_multisets_eq x  A by fastforce
  also have " = card ?S1 + card ((λM. M + {#x#}) ` ?S2)"
    using finite_sets x  A by (subst card_Un_disjoint) auto
  also have " = card ?S1 + card ?S2"
    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