Unification Utilities for Isabelle/ML

Kevin Kappelmann 📧

September 19, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This article provides various unification utilities for Isabelle/ML, most prominently:
  1. First-order and higher-order pattern E-unification and E-matching. While unifiers in Isabelle/ML only consider the $\alpha\beta\eta$-equational theory of the $\lambda$-calculus, unifiers in this article may take an extra background theory, in the form of an equational prover, into account. For example, the unification problem $n + 1 \equiv {}?m + Suc\; 0$ may be solved by providing a prover for the background theory $\forall n.\ n + 1 \equiv n + Suc\; 0$.
  2. Tactics, methods, and attributes with adjustable unifiers (e.g.\ resolution, fact, assumption, OF).
  3. A generalisation of unification hints. Unification hints are a flexible extension for unifiers. Among other things, they can be used for reflective tactics, to provide canonical unification instances, or to simply strengthen the background theory of a unifier in a controlled manner.
  4. Simplifier integration for e-unifiers.
  5. Practical combinations of unification algorithms, e.g. a combination of first-order and higher-order pattern unification.
  6. A hierarchical logger for Isabelle/ML, including per logger configurations with log levels, output channels, message filters.
While this entry works with every object logic, some extra setup for Isabelle/HOL and application examples are provided. All unifiers are tested with SpecCheck.

License

BSD License

Topics

Session ML_Unification