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 hash-functions which are required in the Isabelle Collection Framework and the Container Framework. 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 project. With our new tactics we could remove several tedious proofs for (conditional) linear orders, and conditional equality operators within IsaFoR and the Container Framework.
Theories of Deriving
- van Emde Boas Trees
- A Compositional and Unified Translation of LTL into ω-Automata
- Gröbner Bases Theory
- Derivatives of Logical Formulas
- Haskell’s Show Class in Isabelle/HOL
- Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
- The CAVA Automata Library
- Affine Arithmetic
- Implementing field extensions of the form Q[sqrt(b)]
- Light-weight Containers
- Generating linear orders for datatypes
- Ordinary Differential Equations