Theory Bell_Numbers_Spivey.Bell_Numbers
section ‹Bell Numbers and Spivey's Generalized Recurrence›
theory Bell_Numbers
imports
"HOL-Library.FuncSet"
"HOL-Library.Monad_Syntax"
"HOL-Library.Code_Target_Nat"
"HOL-Combinatorics.Stirling"
Card_Partitions.Injectivity_Solver
Card_Partitions.Card_Partitions
begin
subsection ‹Preliminaries›
subsubsection ‹Additions to FuncSet›
lemma extensional_funcset_ext:
assumes "f ∈ A →⇩E B" "g ∈ A →⇩E B"
assumes "⋀x. x ∈ A ⟹ f x = g x"
shows "f = g"
using assms by (metis PiE_iff extensionalityI)
subsubsection ‹Additions for Injectivity Proofs›
lemma inj_on_impl_inj_on_image:
assumes "inj_on f A"
assumes "⋀x. x ∈ X ⟹ x ⊆ A"
shows "inj_on ((`) f) X"
using assms by (meson inj_onI inj_on_image_eq_iff)
lemma injectivity_union:
assumes "A ∪ B = C ∪ D"
assumes "P A" "P C"
assumes "Q B" "Q D"
"⋀S T. P S ⟹ Q T ⟹ S ∩ T = {}"
shows "A = C ∧ B = D"
using assms Int_Un_distrib Int_commute inf_sup_absorb by blast+
lemma injectivity_image:
assumes "f ` A = g ` A"
assumes "∀x∈A. invert (f x) = x ∧ invert (g x) = x"
shows "∀x∈A. f x = g x"
using assms by (metis (no_types, lifting) image_iff)
lemma injectivity_image_union:
assumes "(λX. X ∪ F X) ` P = (λX. X ∪ G X) ` P'"
assumes "∀X ∈ P. X ⊆ A" "∀X ∈ P'. X ⊆ A"
assumes "∀X ∈ P. ∀y∈F X. y ∉ A" "∀X ∈ P'. ∀y∈G X. y ∉ A"
shows "P = P'"
proof
show "P ⊆ P'"
proof
fix X
assume "X ∈ P"
from assms(1) this obtain X' where "X' ∈ P'" and "X ∪ F X = X' ∪ G X'"
by (metis imageE image_eqI)
moreover from assms(2,4) ‹X ∈ P› have X: "(X ∪ F X) ∩ A = X" by auto
moreover from assms(3,5) ‹X' ∈ P'› have X': "(X' ∪ G X') ∩ A = X'" by auto
ultimately have "X = X'" by simp
from this ‹X' ∈ P'› show "X ∈ P'" by auto
qed
next
show "P' ⊆ P"
proof
fix X'
assume "X' ∈ P'"
from assms(1) this obtain X where "X ∈ P" and "X ∪ F X = X' ∪ G X'"
by (metis imageE image_eqI)
moreover from assms(2,4) ‹X ∈ P› have X: "(X ∪ F X) ∩ A = X" by auto
moreover from assms(3,5) ‹X' ∈ P'› have X': "(X' ∪ G X') ∩ A = X'" by auto
ultimately have "X = X'" by simp
from this ‹X ∈ P› show "X' ∈ P" by auto
qed
qed
subsection ‹Definition of Bell Numbers›
definition Bell :: "nat ⇒ nat"
where
"Bell n = card {P. partition_on {0..<n} P}"
lemma Bell_altdef:
assumes "finite A"
shows "Bell (card A) = card {P. partition_on A P}"
proof -
from ‹finite A› obtain f where bij: "bij_betw f {0..<card A} A"
using ex_bij_betw_nat_finite by blast
from this have inj: "inj_on f {0..<card A}"
using bij_betw_imp_inj_on by blast
from bij have image_f_eq: "A = f ` {0..<card A}"
using bij_betw_imp_surj_on by blast
have "∀x ∈ {P. partition_on {0..<card A} P}. x ⊆ Pow {0..<card A}"
by (auto elim: partition_onE)
from this inj have "inj_on ((`) ((`) f)) {P. partition_on {0..<card A} P}"
by (intro inj_on_impl_inj_on_image[of _ "Pow {0..<card A}"]
inj_on_impl_inj_on_image[of _ "{0..<card A}"]) blast+
moreover from inj have "(`) ((`) f) ` {P. partition_on {0..<card A} P} = {P. partition_on A P}"
by (subst image_f_eq, auto elim!: set_of_partition_on_map)
ultimately have "bij_betw ((`) ((`) f)) {P. partition_on {0..<card A} P} {P. partition_on A P}"
by (auto intro: bij_betw_imageI)
from this ‹finite A› show ?thesis
unfolding Bell_def
by (subst bij_betw_iff_card[symmetric]) (auto intro: finitely_many_partition_on)
qed
lemma Bell_0:
"Bell 0 = 1"
by (auto simp add: Bell_def partition_on_empty)
subsection ‹Construction of the Partitions›
definition construct_partition_on :: "'a set ⇒ 'a set ⇒ 'a set set set"
where
"construct_partition_on B C =
do {
k ← {0..card B};
j ← {0..card C};
P ← {P. partition_on C P ∧ card P = j};
B' ← {B'. B' ⊆ B ∧ card B' = k};
Q ← {Q. partition_on B' Q};
f ← (B - B') →⇩E P;
P' ← {(λX. X ∪ {x ∈ B - B'. f x = X}) ` P};
{P' ∪ Q}
}"
lemma construct_partition_on:
assumes "finite B" "finite C"
assumes "B ∩ C = {}"
shows "construct_partition_on B C = {P. partition_on (B ∪ C) P}"
proof (rule set_eqI')
fix Q'
assume "Q' ∈ construct_partition_on B C"
from this obtain j k P P' Q B' f
where "j ≤ card C"
and "k ≤ card B"
and P: "partition_on C P ∧ card P = j"
and B': "B' ⊆ B ∧ card B' = k"
and Q: "partition_on B' Q"
and f: "f ∈ B - B' →⇩E P"
and P': "P' = (λX. X ∪ {x ∈ B - B'. f x = X}) ` P"
and Q': "Q' = P' ∪ Q"
unfolding construct_partition_on_def by auto
from P f have "partition_on (B - B' ∪ C) P'"
unfolding P' using ‹B ∩ C = {}›
by (intro partition_on_insert_elements) auto
from this Q have "partition_on ((B - B' ∪ C) ∪ B') Q'"
unfolding Q' using B' ‹B ∩ C = {}› by (auto intro: partition_on_union)
from this have "partition_on (B ∪ C) Q'"
using B' by (metis Diff_partition sup.assoc sup.commute)
from this show "Q' ∈ {P. partition_on (B ∪ C) P}" by auto
next
fix Q'
assume Q': "Q' ∈ {Q'. partition_on (B ∪ C) Q'}"
from Q' have "{} ∉ Q'" by (auto elim!: partition_onE)
obtain Q where Q: "Q = ((λX. if X ⊆ B then X else {}) ` Q') - {{}}" by blast
obtain P' where P': "P' = ((λX. if X ⊆ B then {} else X) ` Q') - {{}}" by blast
from P' Q ‹{} ∉ Q'› have Q'_prop: "Q' = P' ∪ Q" by auto
have P'_nosubset: "∀X ∈ P'. ¬ X ⊆ B"
unfolding P' by auto
moreover have "∀X ∈ P'. X ⊆ B ∪ C"
using Q' P' by (auto elim: partition_onE)
ultimately have P'_witness: "∀X ∈ P'. ∃x. x ∈ X ∩ C"
using ‹B ∩ C = {}› by fastforce
obtain B' where B': "B' = ⋃Q" by blast
have Q_prop: "partition_on B' Q"
using B' Q' Q'_prop partition_on_split2 mem_Collect_eq by blast
have "⋃P' = B - B' ∪ C"
proof
have "⋃Q' = B ∪ C" "∀X∈Q'. ∀X'∈Q'. X ≠ X' ⟶ X ∩ X' = {}"
using Q' unfolding partition_on_def disjoint_def by auto
from this show "⋃P' ⊆ B - B' ∪ C"
unfolding P' B' Q by auto blast
next
show "B - B' ∪ C ⊆ ⋃P'"
proof
fix x
assume "x ∈ B - B' ∪ C"
from this obtain X where X: "x ∈ X" "X ∈ Q'"
using Q' by (metis Diff_iff Un_iff mem_Collect_eq partition_on_partition_on_unique)
have "∀X ∈ Q'. X ⊆ B ⟶ X ⊆ B'"
unfolding B' Q by auto
from this X ‹x ∈ B - B' ∪ C› have "¬ X ⊆ B"
using ‹B ∩ C = {}› by auto
from this ‹X ∈ Q'› have "X ∈ P'" using P' by auto
from this ‹x ∈ X› show "x ∈ ⋃P'" by auto
qed
qed
from this have partition_on_P': "partition_on (B - B' ∪ C) P'"
using partition_on_split1 Q'_prop Q' mem_Collect_eq by fastforce
obtain P where P: "P = (λX. X ∩ C) ` P'" by blast
from P partition_on_P' P'_witness have "partition_on C P"
using partition_on_intersect_on_elements by auto
obtain f where f: "f = (λx. if x ∈ B - B' then (THE X. x ∈ X ∧ X ∈ P') ∩ C else undefined)" by blast
have P'_prop: "P' = (λX. X ∪ {x ∈ B - B'. f x = X}) ` P"
proof
{
fix X
assume "X ∈ P'"
have X_subset: "X ⊆ (B - B') ∪ C"
using partition_on_P' ‹X ∈ P'› by (auto elim: partition_onE)
have "X = X ∩ C ∪ {x ∈ B - B'. f x = X ∩ C}"
proof
{
fix x
assume "x ∈ X"
from this X_subset have "x ∈ (B - B') ∪ C" by auto
from this have "x ∈ X ∩ C ∪ {xa ∈ B - B'. f xa = X ∩ C}"
proof
assume "x ∈ C"
from this ‹x ∈ X› show ?thesis by simp
next
assume "x ∈ B - B'"
from partition_on_P' ‹x ∈ X› ‹X ∈ P'› have "(THE X. x ∈ X ∧ X ∈ P') = X"
by (simp add: partition_on_the_part_eq)
from ‹x ∈ B - B'› this show ?thesis unfolding f by auto
qed
}
from this show "X ⊆ X ∩ C ∪ {x ∈ B - B'. f x = X ∩ C}" by auto
next
show "X ∩ C ∪ {xa ∈ B - B'. f xa = X ∩ C} ⊆ X"
proof
fix x
assume "x ∈ X ∩ C ∪ {x ∈ B - B'. f x = X ∩ C}"
from this show "x ∈ X"
proof
assume "x ∈ X ∩ C"
from this show ?thesis by simp
next
assume x_in: "x ∈ {x ∈ B - B'. f x = X ∩ C}"
from this have ex1: "∃!X. x ∈ X ∧ X ∈ P'"
using partition_on_P' by (auto intro!: partition_on_partition_on_unique)
from x_in X_subset have eq: "(THE X. x ∈ X ∧ X ∈ P') ∩ C = X ∩ C"
unfolding f by auto
from P'_nosubset ‹X ∈ P'› have "¬ X ⊆ B" by simp
from this have "X ∩ C ≠ {}"
using X_subset assms(3) by blast
from this obtain y where y: "y ∈ X ∩ C" by auto
from this eq have y_in: "y ∈ (THE X. x ∈ X ∧ X ∈ P') ∩ C" by simp
from y y_in have "y ∈ X" "y ∈ (THE X. x ∈ X ∧ X ∈ P')" by auto
moreover from y have "∃!X. y ∈ X ∧ X ∈ P'"
using partition_on_P' by (simp add: partition_on_partition_on_unique)
moreover have "(THE X. x ∈ X ∧ X ∈ P') ∈ P'"
using ex1 by (rule the1I2) auto
ultimately have "(THE X. x ∈ X ∧ X ∈ P') = X" using ‹X ∈ P'› by auto
from this ex1 show ?thesis by (auto intro: the1I2)
qed
qed
qed
from ‹X ∈ P'› this have "X ∈ (λX. X ∪ {x ∈ B - B'. f x = X}) ` P"
unfolding P by simp
}
from this show "P' ⊆ (λX. X ∪ {x ∈ B - B'. f x = X}) ` P" ..
next
{
fix x
assume x_in_image: "x ∈ (λX. X ∪ {x ∈ B - B'. f x = X}) ` P"
{
fix X
assume "X ∈ P'"
have "{x ∈ B - B'. f x = X ∩ C} = {x ∈ B - B'. x ∈ X}"
proof -
{
fix x
assume "x ∈ B - B'"
from this have ex1: "∃!X. x ∈ X ∧ X ∈ P'"
using partition_on_P' by (auto intro!: partition_on_partition_on_unique)
from this have in_p: "(THE X. x ∈ X ∧ X ∈ P') ∈ P'"
and x_in: "x ∈ (THE X. x ∈ X ∧ X ∈ P')"
by (metis (mono_tags, lifting) theI)+
have "f x = X ∩ C ⟷ (THE X. x ∈ X ∧ X ∈ P') ∩ C = X ∩ C"
using ‹x ∈ B - B'› unfolding f by auto
also have "... ⟷ (THE X. x ∈ X ∧ X ∈ P') = X"
proof
assume "(THE X. x ∈ X ∧ X ∈ P') = X"
from this show "(THE X. x ∈ X ∧ X ∈ P') ∩ C = X ∩ C" by auto
next
assume "(THE X. x ∈ X ∧ X ∈ P') ∩ C = X ∩ C"
have "(THE X. x ∈ X ∧ X ∈ P') ∩ X ≠ {}"
using P'_witness ‹(THE X. x ∈ X ∧ X ∈ P') ∩ C = X ∩ C› ‹X ∈ P'› by fastforce
from this show "(THE X. x ∈ X ∧ X ∈ P') = X"
using partition_on_P'[unfolded partition_on_def disjoint_def] in_p ‹X ∈ P'› by metis
qed
also have "... ⟷ x ∈ X"
using ex1 ‹X ∈ P'› x_in by (auto; metis (no_types, lifting) the_equality)
finally have "f x = X ∩ C ⟷ x ∈ X" .
}
from this show ?thesis by auto
qed
moreover have "X ⊆ B - B' ∪ C"
using partition_on_P' ‹X ∈ P'› by (blast elim: partition_onE)
ultimately have "X ∩ C ∪ {x ∈ B. x ∉ B' ∧ f x = X ∩ C} = X" by auto
}
from this x_in_image have "x ∈ P'" unfolding P by auto
}
from this show "(λX. X ∪ {x ∈ B - B'. f x = X}) ` P ⊆ P'" ..
qed
from partition_on_P' have f_prop: "f ∈ (B - B') →⇩E P"
unfolding f P by (auto simp add: partition_on_the_part_mem)
from Q B' have "B' ⊆ B" by auto
obtain k where k: "k = card B'" by blast
from ‹finite B› ‹B' ⊆ B› k have k_prop: "k ∈ {0..card B}" by (simp add: card_mono)
obtain j where j: "j = card P" by blast
from j ‹partition_on C P› have j_prop: "j ∈ {0..card C}"
by (simp add: assms(2) partition_on_le_set_elements)
from ‹partition_on C P› j have P_prop: "partition_on C P ∧ card P = j" by auto
from k ‹B' ⊆ B› have B'_prop: "B' ⊆ B ∧ card B' = k" by auto
show "Q' ∈ construct_partition_on B C"
using j_prop k_prop P_prop B'_prop Q_prop P'_prop f_prop Q'_prop
unfolding construct_partition_on_def
by (auto simp del: atLeastAtMost_iff) blast
qed
subsection ‹Injectivity of the Set Construction›
lemma injectivity:
assumes "B ∩ C = {}"
assumes P: "(partition_on C P ∧ card P = j) ∧ (partition_on C P' ∧ card P' = j')"
assumes B': "(B' ⊆ B ∧ card B' = k) ∧ (B'' ⊆ B ∧ card B'' = k')"
assumes Q: "partition_on B' Q ∧ partition_on B'' Q'"
assumes f: "f ∈ B - B' →⇩E P ∧ g ∈ B - B'' →⇩E P'"
assumes P': "P'' = (λX. X ∪ {x ∈ B - B'. f x = X}) ` P ∧
P''' = (λX. X ∪ {x ∈ B - B''. g x = X}) ` P'"
assumes eq_result: "P'' ∪ Q = P''' ∪ Q'"
shows "f = g" and "Q = Q'" and "B' = B''"
and "P = P'" and "j = j'" and "k = k'"
proof -
have P_nonempty_sets: "∀X∈P. ∃c∈C. c ∈ X" "∀X∈P'. ∃c∈C. c ∈ X"
using P by (force elim: partition_onE)+
have 1: "∀X∈P''. ∃c∈C. c ∈ X" "∀X∈P'''. ∃c∈C. c ∈ X"
using P' P_nonempty_sets by fastforce+
have 2: "∀X∈Q. ∀x∈X. x ∉ C" "∀X∈Q'. ∀x∈X. x ∉ C"
using ‹B ∩ C = {}› Q B' by (auto elim: partition_onE)
from eq_result have "P'' = P'''" and "Q = Q'"
by (auto dest: injectivity_union[OF _ 1 2])
from this Q show "Q = Q'" and "B' = B''"
by (auto intro!: partition_on_eq_implies_eq_carrier)
have subset_C: "∀X∈P. X ⊆ C" "∀X∈P'. X ⊆ C"
using P by (auto elim: partition_onE)
have eq_image: "(λX. X ∪ {x ∈ B - B'. f x = X}) ` P = (λX. X ∪ {x ∈ B - B''. g x = X}) ` P'"
using P' ‹P'' = P'''› by auto
from this ‹B ∩ C = {}› show "P = P'"
by (auto dest: injectivity_image_union[OF _ subset_C])
have eq2: "(λX. X ∪ {x ∈ B - B'. f x = X}) ` P = (λX. X ∪ {x ∈ B - B'. g x = X}) ` P"
using ‹P = P'› ‹B' = B''› eq_image by simp
from P have P_props: "∀X ∈ P. X ⊆ C" "∀X ∈ P. X ≠ {}" by (auto elim: partition_onE)
have invert: "∀X∈P. (X ∪ {x ∈ B - B'. f x = X}) ∩ C = X ∧ (X ∪ {x ∈ B - B'. g x = X}) ∩ C = X"
using ‹B ∩ C = {}› P_props by auto
have eq3: "∀X ∈ P. (X ∪ {x ∈ B - B'. f x = X}) = (X ∪ {x ∈ B - B'. g x = X})"
using injectivity_image[OF eq2 invert] by blast
have eq4: "∀X ∈ P. {x ∈ B - B'. f x = X} = {x ∈ B - B'. g x = X}"
proof
fix X
assume "X ∈ P"
from this P have "X ⊆ C" by (auto elim: partition_onE)
have disjoint: "X ∩ {x ∈ B - B'. f x = X} = {}" "X ∩ {x ∈ B - B'. g x = X} = {}"
using ‹B ∩ C = {}› ‹X ⊆ C› by auto
from eq3 ‹X ∈ P› have "X ∪ {x ∈ B - B'. f x = X} = X ∪ {x ∈ B - B'. g x = X}" by auto
from this disjoint show "{x ∈ B - B'. f x = X} = {x ∈ B - B'. g x = X}"
by (auto intro: injectivity_union)
qed
from eq4 f have eq5: "∀b∈B - B'. f b = g b" by blast
from eq5 f ‹B' = B''› ‹P = P'› show eq6: "f = g" by (auto intro: extensional_funcset_ext)
from P ‹P = P'› show "j = j'" by simp
from B' ‹B' = B''› show "k = k'" by simp
qed
subsection ‹The Generalized Bell Recurrence Relation›
theorem Bell_eq:
"Bell (n + m) = (∑k≤n. ∑j≤m. j ^ (n - k) * Stirling m j * (n choose k) * Bell k)"
proof -
define A where "A = {0..<n + m}"
define B where "B = {0..<n}"
define C where "C = {n..<n + m}"
have "A = B ∪ C" "B ∩ C = {}" "finite B" "card B = n" "finite C" "card C = m"
unfolding A_def B_def C_def by auto
have step1: "Bell (n + m) = card {P. partition_on A P}"
unfolding Bell_def A_def ..
from ‹A = B ∪ C› ‹B ∩ C = {}› ‹finite B› ‹finite C›
have step2: "card {P. partition_on A P} = card (construct_partition_on B C)"
by (simp add: construct_partition_on)
note injectivity = injectivity[OF ‹B ∩ C = {}›]
let ?expr = "do {
k ← {0..card B};
j ← {0..card C};
P ← {P. partition_on C P ∧ card P = j};
B' ← {B'. B' ⊆ B ∧ card B' = k};
Q ← {Q. partition_on B' Q};
f ← (B - B') →⇩E P;
P' ← {(λX. X ∪ {x ∈ B - B'. f x = X}) ` P};
{P' ∪ Q}
}"
let "?S ⤜ ?comp" = ?expr
{
fix k
assume k: "k ∈ {..card B}"
let ?expr = "?comp k"
let "?S ⤜ ?comp" = ?expr
{
fix j
assume "j ∈ {.. card C}"
let ?expr = "?comp j"
let "?S ⤜ ?comp" = ?expr
from ‹finite C› have "finite ?S"
by (intro finite_Collect_conjI disjI1 finitely_many_partition_on)
{
fix P
assume P: "P ∈ {P. partition_on C P ∧ card P = j}"
from this have "partition_on C P" by simp
let ?expr = "?comp P"
let "?S ⤜ ?comp" = ?expr
have "finite P"
using P ‹finite C› by (auto intro: finite_elements)
from ‹finite B› have "finite ?S" by (auto simp add: finite_subset)
moreover
{
fix B'
assume B': "B' ∈ {B'. B' ⊆ B ∧ card B' = k}"
from this have "B' ⊆ B" by simp
let ?expr = "?comp B'"
let "?S ⤜ ?comp" = ?expr
from ‹finite B› have "finite B'"
using B' by (auto simp add: finite_subset)
from ‹finite B'› have "finite {Q. partition_on B' Q}"
by (rule finitely_many_partition_on)
moreover
{
fix Q
assume Q: "Q ∈ {Q. partition_on B' Q}"
let ?expr = "?comp Q"
let "?S ⤜ ?comp" = ?expr
{
fix f
assume "f ∈ B - B' →⇩E P"
let ?expr = "?comp f"
let "?S ⤜ ?comp" = ?expr
have "disjoint_family_on ?comp ?S"
by (auto intro: disjoint_family_onI)
from this have "card ?expr = 1"
by (simp add: card_bind_constant)
moreover have "finite ?expr"
by (simp add: finite_bind)
ultimately have "finite ?expr ∧ card ?expr = 1" by blast
}
moreover have "finite ?S"
using ‹finite B› ‹finite P› by (auto intro: finite_PiE)
moreover have "disjoint_family_on ?comp ?S"
using P B' Q
by (injectivity_solver rule: local.injectivity(1))
moreover have "card ?S = j ^ (n - k)"
proof -
have "card (B - B') = n - k"
using B' ‹finite B'› ‹card B = n›
by (subst card_Diff_subset) auto
from this show ?thesis
using ‹finite B› P
by (subst card_PiE) (simp add: prod_constant)+
qed
ultimately have "card ?expr = j ^ (n - k)"
by (simp add: card_bind_constant)
moreover have "finite ?expr"
using ‹finite ?S› ‹finite {P. partition_on C P ∧ card P = j}›
by (auto intro!: finite_bind)
ultimately have "finite ?expr ∧ card ?expr = j ^ (n - k)" by blast
} note inner = this
moreover have "card ?S = Bell k"
using B' ‹finite B'› by (auto simp add: Bell_altdef[symmetric])
moreover have "disjoint_family_on ?comp ?S"
using P B'
by (injectivity_solver rule: local.injectivity(2))
ultimately have "card ?expr = j ^ (n - k) * Bell k"
by (subst card_bind_constant) auto
moreover have "finite ?expr"
using inner ‹finite ?S› by (auto intro: finite_bind)
ultimately have "finite ?expr ∧ card ?expr = j ^ (n - k) * Bell k" by blast
} note inner = this
moreover have "card ?S = n choose k"
using ‹card B = n› ‹finite B› by (simp add: n_subsets)
moreover have "disjoint_family_on ?comp ?S"
using P
by (injectivity_solver rule: local.injectivity(3))
ultimately have "card ?expr = j ^ (n - k) * (n choose k) * Bell k"
by (subst card_bind_constant) auto
moreover have "finite ?expr"
using inner ‹finite ?S› by (auto intro: finite_bind)
ultimately have "finite ?expr ∧ card ?expr = j ^ (n - k) * (n choose k) * Bell k" by blast
} note inner = this
moreover note ‹finite ?S›
moreover have "card ?S = Stirling m j"
using ‹finite C› ‹card C = m› by (simp add: card_partition_on)
moreover have "disjoint_family_on ?comp ?S"
by (injectivity_solver rule: local.injectivity(4))
ultimately have "card ?expr = j ^ (n - k) * Stirling m j * (n choose k) * Bell k"
by (subst card_bind_constant) auto
moreover have "finite ?expr"
using inner ‹finite ?S› by (auto intro: finite_bind)
ultimately have "finite ?expr ∧ card ?expr = j ^ (n - k) * Stirling m j * (n choose k) * Bell k" by blast
} note inner = this
moreover have "finite ?S" by simp
moreover have "disjoint_family_on ?comp ?S"
by (injectivity_solver rule: local.injectivity(5))
ultimately have "card ?expr = (∑j≤m. j ^ (n - k) * Stirling m j * (n choose k) * Bell k)" (is "_ = ?formula")
using ‹card C = m› by (subst card_bind) (auto intro: sum.cong)
moreover have "finite ?expr"
using inner ‹finite ?S› by (auto intro: finite_bind)
ultimately have "finite ?expr ∧ card ?expr = ?formula" by blast
}
moreover have "finite ?S" by simp
moreover have "disjoint_family_on ?comp ?S"
by (injectivity_solver rule: local.injectivity(6))
ultimately have step3: "card (construct_partition_on B C) = (∑k≤n. ∑j≤m. j ^ (n - k) * Stirling m j * (n choose k) * Bell k)"
unfolding construct_partition_on_def
using ‹card B = n› by (subst card_bind) (auto intro: sum.cong)
from step1 step2 step3 show ?thesis by auto
qed
subsection ‹Corollaries of the Generalized Bell Recurrence›
corollary Bell_Stirling_eq:
"Bell m = (∑j≤m. Stirling m j)"
proof -
have "Bell m = Bell (0 + m)" by simp
also have "... = (∑j≤m. Stirling m j)"
unfolding Bell_eq[of 0] by (simp add: Bell_0)
finally show ?thesis .
qed
corollary Bell_recursive_eq:
"Bell (n + 1) = (∑k≤n. (n choose k) * Bell k)"
unfolding Bell_eq[of _ 1] by simp
subsection ‹Code equations for the computation of Bell numbers›
text ‹It is slow to compute Bell numbers without dynamic programming (DP). The following is a DP
algorithm derived from the previous recursion formula @{thm [source] Bell_recursive_eq}.›
fun Bell_list_aux :: "nat ⇒ nat list"
where
"Bell_list_aux 0 = [1]" |
"Bell_list_aux (Suc n) = (
let prev_list = Bell_list_aux n;
next_val = (∑(k,z) ← List.enumerate 0 prev_list. z * (n choose (n-k)))
in next_val#prev_list)"
definition Bell_list :: "nat ⇒ nat list"
where "Bell_list n = rev (Bell_list_aux n)"
lemma bell_list_eq: "Bell_list n = map Bell [0..<n+1]"
proof -
have "Bell_list_aux n = rev (map Bell [0..<Suc n])"
proof (induction n)
case 0
then show ?case by (simp add:Bell_0)
next
case (Suc n)
define x where "x = Bell_list_aux n"
define y where "y = (∑(k,z) ← List.enumerate 0 x. z * (n choose (n-k)))"
define sn where "sn = n+1"
have b:"x = rev (map Bell [0..<sn])"
using Suc x_def sn_def by simp
have c: "length x = sn"
unfolding b by simp
have "snd i = Bell (n - fst i)" if "i ∈ set (List.enumerate 0 x)" for i
proof -
have "fst i < length x" "snd i = x ! fst i"
using iffD1[OF in_set_enumerate_eq that] by auto
hence "snd i = Bell (sn - Suc (fst i))"
unfolding b by (simp add:rev_nth)
thus ?thesis
unfolding sn_def by simp
qed
hence "y = (∑i←enumerate 0 x. Bell (n - fst i) * (n choose (n - fst i)))"
unfolding y_def by (intro arg_cong[where f="sum_list"] map_cong refl)
(simp add:case_prod_beta)
also have "... = (∑i←map fst (enumerate 0 x). Bell (n - i) * (n choose (n - i)))"
by (subst map_map) (simp add:comp_def)
also have "... = (∑i = 0..<length x. Bell (n-i) * (n choose (n-i)))"
by (simp add:interv_sum_list_conv_sum_set_nat)
also have "... = (∑i≤n. Bell (n-i) * (n choose (n-i)))"
using c sn_def by (intro sum.cong) auto
also have "... = (∑i ∈ (λk. n- k) ` {..n}. Bell i * (n choose i))"
by (subst sum.reindex, auto simp add:inj_on_def)
also have "... = (∑i ≤ n. Bell i * (n choose i))"
by (intro sum.cong refl iffD2[OF set_eq_iff] allI)
(simp add:image_iff atMost_def, presburger)
also have "... = Bell (Suc n)"
using Bell_recursive_eq by (simp add:mult.commute)
finally have a: "y = Bell (Suc n)" by simp
have "Bell_list_aux (Suc n) = y#x"
unfolding x_def y_def by (simp add:Let_def)
also have "... = Bell (Suc n)#(rev (map Bell [0..<Suc n]))"
unfolding a b sn_def by simp
also have "... = rev (map Bell [0..<Suc (Suc n)])"
by simp
finally show ?case by simp
qed
thus "Bell_list n = map Bell [0..<n+1]"
by (simp add:Bell_list_def)
qed
lemma Bell_eval[code]: "Bell n = last (Bell_list n)"
unfolding bell_list_eq by simp
end