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

- Tools

### Session ML_Unification

- ML_Code_Utils
- ML_Attributes
- ML_Logger
- Setup_Result_Commands
- ML_Logger_Examples
- ML_Attribute_Utils
- ML_Conversion_Utils
- ML_Parsing_Utils
- ML_Functor_Instances
- ML_General_Utils
- ML_Generic_Data_Utils
- ML_Method_Utils
- ML_Priorities
- ML_Normalisations
- ML_Binders
- ML_Term_Utils
- ML_Tactic_Utils
- ML_Theorem_Utils
- ML_Utils
- ML_Unification_Base
- Simps_To
- ML_Unifiers
- ML_Unification_Parsers
- Unify_Assumption_Tactic
- Unify_Resolve_Tactics
- Unify_Fact_Tactic
- Unification_Tactics
- Unification_Attributes
- ML_Term_Index
- ML_Unification_Hints
- ML_Unification_HOL_Setup
- E_Unification_Examples
- Unification_Hints_Reification_Examples
- ML_Unification_Tests_Base
- First_Order_ML_Unification_Tests
- Higher_Order_Pattern_ML_Unification_Tests
- Higher_Order_ML_Unification_Tests
- ML_Unification_Tests

### Depends on

- SpecCheck - Specification-Based Testing for Isabelle/ML

### Used by

- Transport via Partial Galois Connections and Equivalences

### Auto-related entries

- Conditional Transfer Rule

## Cite

×

ML_Unification-AFP

    @article{ML_Unification-AFP,
      author  = {Kevin Kappelmann},
      title   = {Unification Utilities for Isabelle/ML},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/ML_Unification.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest