Generating linear orders for datatypes

Title:	Generating linear orders for datatypes
Author:	René Thiemann
Submission date:	2012-08-07
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.
BibTeX:	@article{Datatype_Order_Generator-AFP, author = {René Thiemann}, title = {Generating linear orders for datatypes}, journal = {Archive of Formal Proofs}, month = aug, year = 2012, note = {\url{http://isa-afp.org/entries/Datatype_Order_Generator.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Deriving, Native_Word
Used by:	Higher_Order_Terms, WOOT_Strong_Eventual_Consistency
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.