Operations on Bounded Natural Functors

Title:	Operations on Bounded Natural Functors
Authors:	Jasmin Christian Blanchette (j /dot/ c /dot/ blanchette /at/ vu /dot/ nl), Andrei Popescu and Dmitriy Traytel
Submission date:	2017-12-19
Abstract:	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.
BibTeX:	@article{BNF_Operations-AFP, author = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel}, title = {Operations on Bounded Natural Functors}, journal = {Archive of Formal Proofs}, month = dec, year = 2017, note = {\url{https://isa-afp.org/entries/BNF_Operations.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.