Theory ML_Unification.ML_Unification_Hints_Base

✐‹creator "Kevin Kappelmann"›
section ‹Unification Hints›
theory ML_Unification_Hints_Base
  imports
    ML_Conversion_Utils
    ML_Functor_Instances
    ML_Generic_Data_Utils
    ML_Costs_Priorities
    ML_Term_Index
    ML_Tactic_Utils
    ML_Term_Utils
    ML_Unifiers_Base
    ML_Unification_Parsers
begin

paragraph ‹Summary›
text ‹A generalisation of unification hints, originally introduced in \<^cite>‹"unif-hints"›.
The general shape of a hint is:
‹⋀y1...yn. (⋀x1...xn1. lhs1 ≡ rhs1) ⟹ ... ⟹ (⋀x1...xnk. lhsk ≡ rhsk) ⟹ lhs ≡ rhs›

Originally, unification hints are restricted to produce equal terms with respect to the prover's
built-in definitional equality (e.g. ‹αβη›-equality). Since we use proof-producing unification, we
can lift this restriction and support unification hints producing equal terms with respect to the
prover's logic (which widely subsumes definitional equality).

More specifically, we support a generalisation of unification hints that
▸ creates provably equal terms,
▸ allows arbitrary, proof-producing functions to perform the matching/unification,
▸ allows non-atomic left-hand sides for premises (cf. \<^cite>‹"unif-hints"›), and
▸ allows additional universal variables in premises.
›

ML_file‹unification_hints_base.ML›
ML_file‹unification_hints.ML›
ML_file‹term_index_unification_hints.ML›

end