DEPTH_CONV : conv -> conv
Applies a conversion repeatedly to all the sub-terms of a term, in bottom-up
DEPTH_CONV c tm repeatedly applies the conversion c to all the subterms of
the term tm, including the term tm itself. The supplied conversion is
applied repeatedly (zero or more times, as is done by REPEATC) to each
subterm until it fails. The conversion is applied to subterms in bottom-up
- FAILURE CONDITIONS
DEPTH_CONV c tm never fails but can diverge if the conversion c can be
applied repeatedly to some subterm of tm without failing.
The following example shows how DEPTH_CONV applies a conversion to all
subterms to which it applies:
Here, there are two beta-redexes in the input term, one of which
occurs within the other. DEPTH_CONV BETA_CONV applies beta-conversion to
innermost beta-redex (\y. y + x) 1 first. The outermost beta-redex is then
(\x. 1 + x) 2, and beta-conversion of this redex gives 1 + 2.
Because DEPTH_CONV applies a conversion bottom-up, the final result may still
contain subterms to which the supplied conversion applies. For example, in:
# DEPTH_CONV BETA_CONV `(\x. (\y. y + x) 1) 2`;;
val it : thm = |- (\x. (\y. y + x) 1) 2 = 1 + 2
the right-hand side of the result still contains a beta-redex,
because the redex `(\y.y)2` is introduced by virtue an application of
BETA_CONV higher-up in the structure of the input term. By contrast, in the
# DEPTH_CONV BETA_CONV `(\f x. (f x) + 1) (\y.y) 2`;;
val it : thm = |- (\f x. f x + 1) (\y. y) 2 = (\y. y) 2 + 1
all beta-redexes are eliminated, because DEPTH_CONV repeats the
supplied conversion (in this case, BETA_CONV) at each subterm (in this case,
at the top-level term).
# DEPTH_CONV BETA_CONV `(\f x. (f x)) (\y.y) 2`;;
val it : thm = |- (\f x. f x) (\y. y) 2 = 2
If the conversion c implements the evaluation of a function in logic, then
DEPTH_CONV c will do bottom-up evaluation of nested applications of it.
For example, the conversion ADD_CONV implements addition of natural number
constants within the logic. Thus, the effect of:
is to compute the sum represented by the input term.
# DEPTH_CONV NUM_ADD_CONV `(1 + 2) + (3 + 4 + 5)`;;
val it : thm = |- (1 + 2) + 3 + 4 + 5 = 15
- SEE ALSO
ONCE_DEPTH_CONV, REDEPTH_CONV, TOP_DEPTH_CONV, TOP_SWEEP_CONV.