Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Twelvefold Way


view this post on Zulip Email Gateway (Aug 22 2022 at 14:44):

From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks to Lukas Bulwahn for this new entry, which can be found here:

https://www.isa-afp.org/entries/Twelvefold_Way.shtml

This entry provides all cardinality theorems of the Twelvefold Way. The Twelvefold Way systematically classifies twelve related combinatorial problems concerning two finite sets, which include counting permutations, combinations, multisets, set partitions and number partitions. This development builds upon the existing formal developments with cardinality theorems for those structures. It provides twelve bijections from the various structures to different equivalence classes on finite functions, and hence, proves cardinality formulae for these equivalence classes on finite functions.

Larry Paulson


Last updated: Apr 27 2024 at 04:17 UTC