Finite multisets (also known as bags) are a fundamental data structure that generalizes finite sets to record the elements' multiplicities. In the Isabelle proof assistant, finite multisets are defined as the subtype of functions from elements to natural numbers consisting of functions that return non-zero multiplicities for finitely many elements. This representation is negative: the elements occur to the left of the function arrow. To allow (co)datatypes to (co)recurse through multisets, an alternative positive representation as quotients of finite lists of elements modulo permutations is used. Using Isabelle, we define two orthogonal generalizations of multisets and the respective positive and negative representations. First, we view countable multisets either as functions from elements to extended natural numbers that return non-zero multiplicities for countably many elements or, alternatively, as quotients of lazy lists modulo infinitary permutations. Second, we view weighted sets either as functions from elements to optional weights from a well-behaved algebraic structure that return None for all but finitely many elements or, alternatively, as quotients of element-weight lists modulo permutation and regrouping by element. For both types, we establish the necessary functorial structure to support (co)recursion and exemplify this support in two case studies.
Paper draft