fixes A::"'a multiset"
  shows  "card { B . B ⊆# A } = prod (λx. count A x + 1) (set_mset A)"

definition PiE_dflt :: "'a set ⇒ 'b ⇒ ('a ⇒ 'b set) ⇒ ('a ⇒ 'b) set"
  where "PiE_dflt A dflt B = {f. ∀x. (x ∈ A ⟶ f x ∈ B x) ∧ (x ∉ A ⟶ f x = dflt)}"

lemma restrict_PiE_dflt: "(λh. restrict h A) ` PiE_dflt A dflt B = PiE A B"
proof (intro equalityI subsetI)
  fix h assume "h ∈ (λh. restrict h A) ` PiE_dflt A dflt B"
  thus "h ∈ PiE A B"
    by (auto simp: PiE_dflt_def)
next
  fix h assume h: "h ∈ PiE A B"
  hence "restrict (λx. if x ∈ A then h x else dflt) A ∈ (λh. restrict h A) ` PiE_dflt A dflt B"
    by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def)
  also have "restrict (λx. if x ∈ A then h x else dflt) A = h"
    using h by (auto simp: fun_eq_iff)
  finally show "h ∈ (λh. restrict h A) ` PiE_dflt A dflt B" .
qed

lemma card_PiE_dflt:
  assumes "finite A" "⋀x. x ∈ A ⟹ finite (B x)"
  shows   "card (PiE_dflt A d B) = (∏x∈A. card (B x))"
proof -
  from assms have "(∏x∈A. card (B x)) = card (PiE A B)"
    by (intro card_PiE [symmetric]) auto
  also have "PiE A B = (λf. restrict f A) ` PiE_dflt A d B"
    by (rule restrict_PiE_dflt [symmetric])
  also have "card … = card (PiE_dflt A d B)"
    by (intro card_image) (force simp: inj_on_def restrict_def fun_eq_iff PiE_dflt_def)
  finally show ?thesis ..
qed

lemma bij_betw_submultisets:
  "bij_betw count {B. B ⊆# A} (PiE_dflt (set_mset A) 0 (λx. {0..count A x}))"
proof -
  have is_multiset: "h ∈ multiset"
    if "h ∈ PiE_dflt (set_mset A) 0 (λx. {0..count A x})" for h
  proof -
    have "finite {x. h x > 0}"
      by (rule finite_subset[of _ "set_mset A"]) (use that in ‹force simp: PiE_dflt_def›)+
    thus ?thesis by (simp add: multiset_def)
  qed

  show "bij_betw count {B. B ⊆# A} (PiE_dflt (set_mset A) 0 (λx. {0..count A x}))"
  proof (rule bij_betwI[where g = Abs_multiset], goal_cases)
    case 1
    thus ?case
      by (auto simp: PiE_dflt_def mset_subset_eq_count dest: mset_subset_eqD)
  next
    case 2
    show ?case
      by (force simp: PiE_dflt_def subseteq_mset_def is_multiset)
  next
    case 3
    thus ?case
      by (auto simp: PiE_dflt_def)
  next
    case 4
    thus ?case
      by (auto simp: is_multiset PiE_dflt_def)
  qed
qed

lemma "card {B. B ⊆# A} = (∏x∈set_mset A. count A x + 1)"
proof -
  have "card {B. B ⊆# A} = card (PiE_dflt (set_mset A) 0 (λx. {0..count A x}))"
    using bij_betw_submultisets[of A] bij_betw_same_card by blast
  also have "… = (∏x∈set_mset A. count A x + 1)"
    by (subst card_PiE_dflt) auto
  finally show ?thesis .
qed

theory Scratch
  imports Main "HOL-Library.Multiset" "HOL-Library.FuncSet"
begin

lemma bij_betw_submultisets:
  "card {B. B ⊆# A} = (∏x∈set_mset A. count A x + 1)"
proof -
  define f :: "'a multiset ⇒ 'a ⇒ nat"
    where "f = (λB x. if x ∈# A then count B x else undefined)"
  define g :: "('a ⇒ nat) ⇒ 'a multiset"
    where "g = (λh. Abs_multiset (λx. if x ∈# A then h x else 0))"

  have count_g: "count (g h) x = (if x ∈# A then h x else 0)"
    if "h ∈ (Π⇩E x∈set_mset A. {0..count A x})" for h x
  proof -
    have "finite {x. (if x ∈# A then h x else 0) > 0}"
      by (rule finite_subset[of _ "set_mset A"]) (use that in auto)
    thus ?thesis by (simp add: multiset_def g_def)
  qed

  have f: "f B ∈ (Π⇩E x∈set_mset A. {0..count A x})" if "B ⊆# A" for B
      using that by (auto simp: f_def subseteq_mset_def)

  have "bij_betw f {B. B ⊆# A} (Π⇩E x∈set_mset A. {0..count A x})"
  proof (rule bij_betwI[where g = g], goal_cases)
    case 1
    thus ?case using f by auto
  next
    case 2
    show ?case
      by (auto simp: Pi_def PiE_def count_g subseteq_mset_def)
  next
    case (3 B)
    have "count (g (f B)) x  = count B x" for x
    proof -
      have "count (g (f B)) x = (if x ∈# A then f B x else 0)"
        using f 3 by (simp add: count_g)
      also have "… = count B x"
        using 3 by (auto simp: f_def dest: mset_subset_eqD)
      finally show ?thesis .
    qed
    thus ?case
      by (auto simp: multiset_eq_iff)
  next
    case 4
    thus ?case
      by (auto simp: fun_eq_iff f_def count_g)
  qed
  hence "card {B. B ⊆# A} = card (Π⇩E x∈set_mset A. {0..count A x})"
    using bij_betw_same_card by blast
  thus ?thesis
    by (simp add: card_PiE)
qed