Generating linear orders for datatypes

René Thiemann 🌐

August 7, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

This development is aimed at datatypes generated by the "old_datatype" command.

License

BSD License

Topics

Session Datatype_Order_Generator