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 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.
License
Topics
Session Deriving
- Derive_Manager
- Generator_Aux
- Comparator
- Compare
- RBT_Compare_Order_Impl
- RBT_Comparator_Impl
- Comparator_Generator
- Compare_Generator
- Compare_Instances
- Compare_Order_Instances
- Compare_Rat
- Compare_Real
- Equality_Generator
- Equality_Instances
- Hash_Generator
- Hash_Instances
- Countable_Generator
- Derive
- Derive_Examples
Depends on
Used by
- Ordinary Differential Equations
- Generating linear orders for datatypes
- Light-weight Containers
- Implementing field extensions of the form Q[sqrt(b)]
- Affine Arithmetic
- The CAVA Automata Library
- Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
- Haskell's Show Class in Isabelle/HOL
- Derivatives of Logical Formulas
- Gröbner Bases Theory
- A Compositional and Unified Translation of LTL into ω-Automata
- van Emde Boas Trees
- Making Arbitrary Relational Calculus Queries Safe-Range
- Labeled Transition Systems
- A Preprocessor for Linear Diophantine Equalities and Inequalities