Abstract

We present an Isabelle/HOL development that allows for the automatic generation of certain operations for user-defined datatypes. Since the operations are defined within the logic, they are applicable for code generation. Triggered by the demand to provide readable error messages as well as to access efficient data structures like sorted trees in generated code, we provide show functions that compute the string representation of a given value, comparators that yield linear orders, and hash functions. Moreover, large parts of the employed machinery should be reusable for other operations like read functions, etc.

In contrast to similar mechanisms, like Haskell’s “deriving,” we do not only generate definitions, but also prove some desired properties, e.g., that a comparator indeed orders values linearly. This is achieved by a collection of tactics that discharge the corresponding proof obligations automatically.

BibTeX

@inproceedings{CSRT-ITP15,
  author    = "Christian Sternagel and Ren{\'e} Thiemann",
  title     = "Deriving Comparators and Show Functions in {Isabelle/HOL}",
  booktitle = "Proceedings of the 6th International Conference on
               Interactive Theorem Proving (ITP 2015)",
  editor    = "Christian Urban and Xingyuan Zhang",
  series    = "Lecture Notes in Computer Science",
  volume    = 9236,
  pages     = "421--437",
  year      = 2015,
  doi       = "10.1007/978-3-319-22102-1_28"
}