HOL: Reference

match_terml

Term.match_terml
     : hol_type list -> term set -> term -> term
       -> (term,term) subst * (hol_type,hol_type) subst

Match two terms while restricting some instantiations.

An invocation match_terml avoid_tys avoid_tms pat ob (tmS,tyS), if it does not raise an exception, returns a pair of substitutions (S,T) such that

   aconv (subst S (inst T pat)) ob.

The arguments avoid_tys and avoid_tms specify type and term variables in pat that are not allowed to become redexes in S and T.

Failure

match_terml will fail if no S and T meeting the above requirements can be found. If a match (S,T) between pat and ob can be found, but elements of avoid_tys would appear as redexes in T or elements of avoid_tms would appear as redexes in S, then match_terml will also fail.

Example

> val (tmS,tyS) = match_terml [] empty_varset
                 (Term `\x:'a. x = f (y:'b)`)
                 (Term `\a.    a = ~p`);
val tmS = [{redex = “f”, residue = “$¬”}, {redex = “y”, residue = “p”}]:
   (term, term) Term.subst
val tyS =
   [{redex = “:β”, residue = “:bool”}, {redex = “:α”, residue = “:bool”}]:
   (hol_type, hol_type) Term.subst

> match_terml [alpha] empty_varset  (* forbid instantiation of 'a *)
        (Term `\x:'a. x = f (y:'b)`)
        (Term `\a.    a = ~p`);
Exception- HOL_ERR (at Type.raw_match_type: double bind on type variable 'a) raised

> match_terml [] (HOLset.add(empty_varset,mk_var("y",beta)))
        (Term `\x:'a. x = f (y:'b)`)
        (Term `\a.    a = ~p`);
Exception- HOL_ERR (at Term.raw_match_term: double bind on variable "y") raised

See also

Term.match_term, Term.raw_match, Term.subst, Term.inst, Type.match_typel, Type.type_subst