----------------------------------------------------------------------
PSUB_CONV                                                  (PairRules)
----------------------------------------------------------------------
PSUB_CONV : (conv -> conv)

KEYWORDS
conversional.

LIBRARY
pair

SYNOPSIS
Applies a conversion to the top-level subterms of a term.

DESCRIBE
For any conversion {c}, the function returned by {PSUB_CONV c} is a conversion
that applies {c} to all the top-level subterms of a term.  If the conversion
{c} maps {t} to {|- t = t'}, then {SUB_CONV c} maps a paired
abstraction {"\p.t"} to the theorem:

   |- (\p.t) = (\p.t')

That is, {PSUB_CONV c "\p.t"} applies {c} to the body of the
paired abstraction {"\p.t"}.
If {c} is a conversion that maps {"t1"} to the theorem
{|- t1 = t1'} and {"t2"} to the theorem {|- t2 = t2'}, then the conversion
{PSUB_CONV c} maps an application {"t1 t2"} to the theorem:

   |- (t1 t2) = (t1' t2')

That is, {PSUB_CONV c "t1 t2"} applies {c} to the both the operator
{t1} and the operand {t2} of the application {"t1 t2"}.  Finally, for any
conversion {c}, the function returned by {PSUB_CONV c} acts as the identity
conversion on variables and constants.  That is, if {"t"} is a variable or
constant, then {PSUB_CONV c "t"} returns {|- t = t}.

FAILURE
{PSUB_CONV c tm} fails if {tm} is a paired abstraction {"\p.t"} and the
conversion {c} fails when applied to {t},
or if {tm} is an application {"t1 t2"} and the
conversion {c} fails when applied to either {t1} or {t2}.  The function
returned by {PSUB_CONV c} may also fail if the ML function {c:term->thm} is not,
in fact, a conversion (i.e. a function that maps a term {t} to a theorem
{|- t = t'}).

SEEALSO
Conv.SUB_CONV, PairRules.PABS_CONV, Conv.RAND_CONV, Conv.RATOR_CONV.

----------------------------------------------------------------------