STRIP_QUANT_CONV

Conv.STRIP_QUANT_CONV : conv -> conv

Applies a conversion underneath a quantifier prefix.

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.

See also

Conv.STRIP_BINDER_CONV, Conv.QUANT_CONV, Conv.BINDER_CONV, Conv.ABS_CONV