----------------------------------------------------------------------
PAT_CONV                                                        (Conv)
----------------------------------------------------------------------
PAT_CONV : term -> conv -> conv

SYNOPSIS
Applies a conversion at specific sub-terms, following a pattern

KEYWORDS
rewriting

DESCRIBE
The call {PAT_CONV ``\x1 ... xn. t[x1,...,xn]`` cnv} returns a new
conversion that applies {cnv} to subterms of the target term
corresponding to the free instances of any {xi} in the pattern
{t[x1,...,xn]}. The fact that the pattern is a function has no logical
significance; it is just used as a convenient format for the pattern.



FAILURE
Never fails until applied to a term, but then it may fail if the core conversion does on the chosen subterms, or if the pattern doesn’t match the structure of the term.



EXAMPLE
Here we choose to evaluate just two subterms:

   > PAT_CONV ``\x. x + a + x`` numLib.REDUCE_CONV
              ``(1 + 2) + (3 + 4) + (5 + 6)``;
   val it : thm = |- 1 + 2 + (3 + 4) + (5 + 6) = 3 + (3 + 4) + 11

while here we swap two particular quantifiers in a long chain:

   > PAT_CONV ``\x. !x1 x2 x3 x4 x5. x`` SWAP_FORALL_CONV
              ``!a b c d e f g h. something``
   <<HOL message: inventing new type variable names: ...>>
   val it =
     |- (!a b c d e f g h. something) <=>
        !a b c d e g f h. something: thm


COMMENTS
Multiple bound variables will only be necessary if the conversion
needs to be applied to sub-terms of different types.

SEEALSO
Conv.ABS_CONV, Conv.COMB_CONV, Conv.PATH_CONV, Conv.RAND_CONV,
Conv.RATOR_CONV, Conv.SUB_CONV.

----------------------------------------------------------------------