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.
- Making Arbitrary Relational Calculus Queries Safe-Range
- 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