match_term : term -> term -> (term,term) subst * (hol_type,hol_type) subst

- STRUCTURE
- SYNOPSIS
- Finds instantiations to match one term to another.
- DESCRIPTION
- An application match_term M N attempts to find a set of type and term instantiations for M to make it alpha-convertible to N. If match_term succeeds, it returns the instantiations in the form of a pair containing a term substitution and a type substitution. In particular, if match_term pat ob succeeds in returning a value (S,T), then
aconv (subst S (inst T pat)) ob.

- FAILURE
- Fails if the term cannot be matched by one-way instantiation. If the pattern includes variables of the same name but different types, the resulting type instantiation may cause those variables to be identified and the term instantiation to be useless.
- EXAMPLE
- The following shows how match_term could be used to match the conclusion of a theorem to a term.The following shows an attempt to use a bad pattern (the pattern term t has two variables called x at different types):
> val th = REFL (Term `x:'a`); val th = |- x = x : thm > match_term (concl th) (Term `1 = 1`); val it = ([{redex = `x`, residue = `1`}], [{redex = `:'a`, residue = `:num`}]) : term subst * hol_type subst > INST_TY_TERM it th; val it = |- 1 = 1

The tminst value is unusable as it seeks to instantiate two different x variables (one with a, one with b) that are now actually the same variable.> val _ = show_types := true; > val t = list_mk_comb(``f:'a -> 'b -> 'c``, [``x:'a``, ``x:'b``]); val t = ``(f : 'a -> 'b -> 'c) (x:'a) (x:'b)``; > val (tminst, tyinst) = match_term t ``(g: 'a -> 'a -> 'b) a b``; val tminst = [{redex = ``(f :'a -> 'a -> 'b)``, residue = ``(g :'a -> 'a -> 'b)``}, {redex = ``(x :'a)``, residue = ``(a :'a)``}, {redex = ``(x :'a)``, residue = ``(b :'a)``}]: (term, term) Term.subst val tyinst = [{redex = ``:'c``, residue = ``:'b``}, {redex = ``:'b``, residue = ``:'a``}]: (hol_type, hol_type) Term.subst

- COMMENTS
- For instantiating theorems PART_MATCH is usually easier to use.
- SEEALSO

HOL Kananaskis-13