### 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.

### License

BSD License

### Topics

- Tools

### Session BNF_Operations

- LFP
- GFP
- Compose
- Kill
- Lift
- Permute
- N2M

## Cite

×

BNF_Operations-AFP

    @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   = {December},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/BNF_Operations.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018