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
- 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