Term.match

STRUCTURE

SYNOPSIS

Match two terms while restricting some instantiations.

DESCRIPTION

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 (S,T) = match_terml [] empty_varset
                  (Term `\x:'a. x = f (y:'b)`)
                  (Term `\a.    a = ~p`);
> val S = [{redex = `(f :'b -> 'a)`, residue = `$~`},
           {redex = `(y :'b)`,       residue = `(p :bool)`}] : ...

  val T = [{redex = `:'b`, residue = `:bool`},
           {redex = `:'a`, residue = `:bool`}] : ...

- match_terml [alpha] empty_varset  (* forbid instantiation of 'a *)
          (Term `\x:'a. x = f (y:'b)`)
          (Term `\a.    a = ~p`);
! Uncaught exception:
! HOL_ERR

- match_terml [] (HOLset.add(empty_varset,mk_var("y",beta)))
          (Term `\x:'a. x = f (y:'b)`)
          (Term `\a.    a = ~p`);
! Uncaught exception:
! HOL_ERR

SEEALSO

match_term, raw_match, subst, inst, match_typel, type_subst