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