Email Gateway (Jun 17 2026 at 16:59): Email Gateway (Jun 17 2026 at 16:59):From: Tobias Nipkow <nipkow@in.tum.de>
Formalization of Weighted Sets
Mathias Schack Rabing and Dmitriy Traytel
We define weighted sets as a generalization of finite multisets where
multiplicities are replaced by weights from a refinable abelian semigroup.
Weighted sets are equivalently represented as functions from elements to
optional weights returning None for all but finitely many elements, or as
quotients of element-weight lists modulo permutation and regrouping. We register
weighted sets as a bounded natural functor (BNF), enabling nested (co)recursion
through them in (co)datatypes.
https://isa-afp.org/entries/Weighted_Set.html
Enjoy!
Last updated: Jul 02 2026 at 07:34 UTC