1\DOC STRIP_QUANT_CONV
2
3\TYPE {STRIP_QUANT_CONV : conv -> conv}
4
5\SYNOPSIS
6Applies a conversion underneath a quantifier prefix.
7
8\KEYWORDS
9conversion, quantifier.
10
11\DESCRIBE
12If {tm} has the form {Q(\v1. ... (Q(\vn.M))...)} and the application of
13{conv} to {M} yields {|- M = N}, then {STRIP_QUANT_CONV conv tm}
14returns {|- Q(\v1. ... (Q(\vn.M))...) = Q(\v1. ... (Q(\vn.N))...)},
15provided {Q} is Hilbert's choice operator or a universal, existential, or
16unique-existence quantifer.
17
18Otherwise, {STRIP_QUANT_CONV conv tm} returns {conv tm}.
19
20\FAILURE
21If {conv M} fails. Or if {conv tm} fails when {tm} is not a quantified term.
22Also fails if some of {[v1,...,vn]} are free in the hypotheses of {conv M}.
23
24\EXAMPLE
25{
26- STRIP_QUANT_CONV (STRIP_QUANT_CONV SYM_CONV)
27    (Term `!x y z. ?!p q r. x + y*z = p*q + r`);
28
29> val it =
30    |- (!x y z. ?!p q r. x + y * z = p * q + r) =
31        !x y z. ?!p q r. p * q + r = x + y * z : thm
32}
33
34\COMMENTS
35To deal with binders not in the above list, e.g., newly introduced ones,
36use {STRIP_BINDER_CONV}.
37
38For deeply nested quantifiers, {STRIP_QUANT_CONV} and {STRIP_BINDER_CONV}
39are more efficient than iterated application of {QUANT_CONV}, {BINDER_CONV},
40or {ABS_CONV}.
41
42\SEEALSO
43Conv.STRIP_BINDER_CONV, Conv.QUANT_CONV, Conv.BINDER_CONV, Conv.ABS_CONV.
44
45\ENDDOC
46