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