1\DOC SUB_CONV
2
3\TYPE {SUB_CONV : conv -> conv}
4
5\SYNOPSIS
6Applies a conversion to the top-level subterms of a term.
7
8\KEYWORDS
9conversional.
10
11\DESCRIBE
12For any conversion {c}, the function returned by {SUB_CONV c} is a
13conversion that applies {c} to all the top-level subterms of a term.
14Its implementation is
15{
16  fun SUB_CONV c = TRY_CONV (COMB_CONV c ORELSEC ABS_CONV c)
17}
18
19\EXAMPLE
20If the conversion {c} maps {t} to {|- t = t'}, then {SUB_CONV c} maps
21an abstraction {``\x.t``} to the theorem:
22{
23   |- (\x.t) = (\x.t')
24}
25That is, {SUB_CONV c ``\x.t``} applies {c} to the body of the
26abstraction {``\x.t``}.  If {c} is a conversion that maps {``t1``} to the
27theorem {|- t1 = t1'} and {``t2``} to the theorem {|- t2 = t2'}, then
28the conversion {SUB_CONV c} maps an application {``t1 t2``} to the
29theorem:
30{
31   |- (t1 t2) = (t1' t2')
32}
33That is, {SUB_CONV c ``t1 t2``} applies {c} to the both the operator
34{t1} and the operand {t2} of the application {``t1 t2``}.  Finally, for
35any conversion {c}, the function returned by {SUB_CONV c} acts as the
36identity conversion on variables and constants.  That is, if {``t``} is
37a variable or constant, then {SUB_CONV c ``t``} raises the {UNCHANGED} exception.
38
39\FAILURE
40{SUB_CONV c tm} fails if {tm} is an abstraction {``\x.t``} and the
41conversion {c} fails when applied to {t}, or if {tm} is an application
42{``t1 t2``} and the conversion {c} fails when applied to either {t1} or
43{t2}.  The function returned by {SUB_CONV c} may also fail if the ML
44function {c:term->thm} is not, in fact, a conversion (i.e. a function
45that maps a term {t} to a theorem {|- t = t'}).
46
47\SEEALSO
48Conv.ABS_CONV, Conv.COMB_CONV, Conv.RAND_CONV, Conv.RATOR_CONV.
49\ENDDOC
50