Abstract

We provide a framework for registering automatic methods to derive class instances of datatypes, as it is possible using Haskell’s “deriving Ord, Show, ...” feature.

We further implemented such automatic methods to derive comparators, linear orders, parametrizable equality functions, and hash-functions which are required in the Isabelle Collection Framework and the Container Framework. Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. All of the generators are based on the infrastructure that is provided by the BNF-based datatype package.

Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework.

BibTeX

@article{CSRT-AFP15a,
  author  = {Christian Sternagel and René Thiemann},
  title   = {Deriving class instances for datatypes},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2015,
  note    = {\url{https://www.isa-afp.org/entries/Deriving.html},
            Formal proof development},
  ISSN    = {2150-914x},
}