We present a collection of formalized results pertaining to (finite) nested multisets, developed using the Isabelle/HOL proof assistant. The nested multiset order is a generalization of the multiset order that can be used to prove termination of processes. Hereditary multisets, a variant of nested multisets, offer a convenient representation of ordinals below ε0. In Isabelle, both nested and hereditary multisets can be comfortably defined as inductive datatypes. Our formal library also provides, somewhat nonstandardly, multisets with negative multiplicities and ordinals with negative coefficients. We present some applications of the library to formalizations of Goodstein’s theorem and the decidability of unary programming computable functions (PCF).
Paper draft