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.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|