I am looking for an existing proof of this:

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

or alternatively a lemma that makes this trivial.

Usually, the best way to show a cardinality is to show a bijection to objects where the cardinality is obvious. In this case, an indexed product. It's a bit fiddly here since we need the elements outside the domain to get mapped to 0 (the standard approach using `PiE`

from `HOL-Library.FuncSets`

maps them to `undefined`

. I therefore borrow `PiE_dflt`

from one of my AFP entries for this:

```
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
```

Actually, here's a more direct proof without all that `PiE_dflt`

business:

```
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
```

Interesting to see that `set_mset (Pow_mset A)`

can be useful. I did not expect that. (`Pow_mset`

exists only in a theory in my mailbox so far...)

for the sake of completeness, there are three concepts that are very linked:

`{B. B ⊆# A}`

`Pow_mset`

(the multiset version of Pow)`subseqs`

(by`Pow_mset (mset A) = image_mset mset (mset (subseqs A))`

), aka`{B. B ⊆# A} = image mset (set (subseqs A))`

I (I should say https://search.isabelle.in.tum.de/) did not find any lemma on cardinality and subseqs to avoid Manuel's proof above.

(`Subseqs`

also exists, but only in https://search.isabelle.in.tum.de/#theory/default_Isabelle2020_AFP2020/Regular-Sets.Regexp_Constructions)

Thank you @Manuel Eberl and @Mathias Fleury for the responses.

Last updated: Sep 25 2022 at 22:23 UTC