Operations on Bounded Natural Functors

Jasmin Christian Blanchette 📧, Andrei Popescu 🌐 and Dmitriy Traytel 🌐

December 19, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry formalizes the closure property of bounded natural functors (BNFs) under seven operations. These operations and the corresponding proofs constitute the core of Isabelle's (co)datatype package. To be close to the implemented tactics, the proofs are deliberately formulated as detailed apply scripts. The (co)datatypes together with (co)induction principles and (co)recursors are byproducts of the fixpoint operations LFP and GFP. Composition of BNFs is subdivided into four simpler operations: Compose, Kill, Lift, and Permute. The N2M operation provides mutual (co)induction principles and (co)recursors for nested (co)datatypes.


BSD License


Session BNF_Operations