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 (linear) orders or hash-functions which are required in the Isabelle Collection Framework. Moreover, for the tactic of Huffman and Krauss to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework.

Our formalization was performed as part of the IsaFoR/CeTA project. With our new tactic we could completely remove tedious proofs for linear orders of two datatypes.

BibTeX

@article{RT-AFP12b,
  author  = {René Thiemann},
  title   = {Generating linear orders for datatypes},
  journal = "Archive of Formal Proofs",
  month   = aug,
  year    = 2012,
  note    = {\url{http://afp.sf.net/entries/Datatype_Order_Generator.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}