Spivey's Generalized Recurrence for Bell Numbers


Title: Spivey's Generalized Recurrence for Bell Numbers
Author: Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com)
Submission date: 2016-05-04
Abstract: This entry defines the Bell numbers as the cardinality of set partitions for a carrier set of given size, and derives Spivey's generalized recurrence relation for Bell numbers following his elegant and intuitive combinatorial proof.

As the set construction for the combinatorial proof requires construction of three intermediate structures, the main difficulty of the formalization is handling the overall combinatorial argument in a structured way. The introduced proof structure allows us to compose the combinatorial argument from its subparts, and supports to keep track how the detailed proof steps are related to the overall argument. To obtain this structure, this entry uses set monad notation for the set construction's definition, introduces suitable predicates and rules, and follows a repeating structure in its Isar proof.

  author  = {Lukas Bulwahn},
  title   = {Spivey's Generalized Recurrence for Bell Numbers},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Bell_Numbers_Spivey.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Card_Number_Partitions, Card_Partitions
Used by: Card_Equiv_Relations, Twelvefold_Way
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.