Nominal Isabelle provides powerful tools for meta-theoretic reasoning about syntax of logics or programming languages, in which variables are bound. It has been instrumental to major verification successes, such as Gödel's incompleteness theorems. However, the existing tooling is not compositional. In particular, it does not support nested recursion and flattens complex binders to lists, sets, or multisets, which for example prevents the correct definition of alpha-equivalence in the presence of nested linear patterns. Moreover, there is no support for infinitely branching syntax. These limitations are fundamental in the way nominal datatypes and functions on them are constructed within Nominal Isabelle. Following recent theoretical advancements that overcome these limitations through a modular approach, we develop and implement a new definitional package for binding-aware datatypes in Isabelle/HOL. We describe the journey from the user specification to the end product consisting of the desired types, reasoning principles about them, and a binding-aware primitive recursion module. We validate our work in two formalization case studies that so far were out of reach of nominal approaches: (1) the POPLmark 2B challenge, which involves non-free binders for linear pattern matching and (2) Mazza's infinitary affine lambda calculus.
Paper draft