This formalisation is now part of the AFP. Please refer to https://www.isa-afp.org/entries/ML_Unification.html
- First-order and higher-order pattern
[E-unification](https://en.wikipedia.org/wiki/Unification_(computer_science%29#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 = ?m + Suc 0
may be solved by providing a prover for the background theoryforall n. n + 1 = n + Suc 0
. - Tactics, methods, and attributes with adjustable unifiers (e.g.\ resolution, fact, assumption, OF).
- 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.
- Simplifier integration for e-unifiers.
- Practical combinations of unification algorithms, e.g. a combination of first-order and higher-order pattern unification.
- A hierarchical logger for Isabelle/ML,
including per logger configurations with log levels, output channels, message filters.
See
Logger/README.md
for details.
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.
See Examples/
for some application examples.
Requirements:
- The Isabelle development version
- The AFP development version
- Add higher-order unifier E-unification and matching
- tests:
- adapt tests to work for open terms