PAT_CONV
Conv.PAT_CONV : term -> conv -> conv
Applies a conversion at specific sub-terms, following a pattern
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.
See also
Conv.ABS_CONV, Conv.COMB_CONV,
Conv.PATH_CONV,
Conv.RAND_CONV,
Conv.RATOR_CONV, Conv.SUB_CONV