STRIP_QUANT_CONV : conv -> conv
STRUCTURE
Conv
SYNOPSIS
Applies a conversion underneath a quantifier prefix.
DESCRIPTION
If tm has the form Q(\v1. ... (Q(\vn.M))...) and the application of conv to M yields |- M = N, then STRIP_QUANT_CONV conv tm returns |- Q(\v1. ... (Q(\vn.M))...) = Q(\v1. ... (Q(\vn.N))...), provided Q is Hilbert’s choice operator or a universal, existential, or unique-existence quantifer.

Otherwise, STRIP_QUANT_CONV conv tm returns conv tm.

FAILURE
If conv M fails. Or if conv tm fails when tm is not a quantified term. Also fails if some of [v1,...,vn] are free in the hypotheses of conv M.
EXAMPLE
- STRIP_QUANT_CONV (STRIP_QUANT_CONV SYM_CONV)
    (Term `!x y z. ?!p q r. x + y*z = p*q + r`);

> val it =
    |- (!x y z. ?!p q r. x + y * z = p * q + r) =
        !x y z. ?!p q r. p * q + r = x + y * z : thm
COMMENTS
To deal with binders not in the above list, e.g., newly introduced ones, use STRIP_BINDER_CONV.

For deeply nested quantifiers, STRIP_QUANT_CONV and STRIP_BINDER_CONV are more efficient than iterated application of QUANT_CONV, BINDER_CONV, or ABS_CONV.

SEEALSO
STRIP_BINDER_CONV, QUANT_CONV, BINDER_CONV, ABS_CONV
HOL  Kananaskis-14