Deriving class instances for datatypes

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 comparators, linear orders, parametrizable equality functions, and hashfunctions which are required in the Isabelle Collection Framework [1] and the Container Framework [2]. Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework. All of the generators are based on the infrastructure that is provided by the BNF-based datatype package. Our formalization was performed as part of the IsaFoR/CeTA project1 [3]. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework. Contents 1 Derive Manager 3 2 Shared Utilities for all Generator 3 3 Comparisons 4 3....

• Type: Journal
• Year: 2015
• Where: AFP
• Authors: Christian Sternagel, René Thiemann
• Keywords: AFP 2015, Formal Methods