ONCE_DEPTH_CONV : conv -> conv
Applies a conversion once to the first suitable sub-term(s) encountered in
ONCE_DEPTH_CONV c tm applies the conversion c once to the first subterm or
subterms encountered in a top-down `parallel' search of the term tm for which
c succeeds. If the conversion c fails on all subterms of tm, the theorem
returned is |- tm = tm.
- FAILURE CONDITIONS
The following example shows how ONCE_DEPTH_CONV applies a conversion to only
the first suitable subterm(s) found in a top-down search:
Here, there are two beta-redexes in the input term. One of these
occurs within the other, so BETA_CONV is applied only to the outermost one.
Note that the supplied conversion is applied by ONCE_DEPTH_CONV to all
independent subterms at which it succeeds. That is, the conversion is applied
to every suitable subterm not contained in some other subterm for which the
conversions also succeeds, as illustrated by the following example:
# ONCE_DEPTH_CONV BETA_CONV `(\x. (\y. y + x) 1) 2`;;
val it : thm = |- (\x. (\y. y + x) 1) 2 = (\y. y + 2) 1
Here num_CONV is applied to both 1 and 2, since neither term
occurs within a larger subterm for which the conversion num_CONV succeeds.
# ONCE_DEPTH_CONV num_CONV `(\x. (\y. y + x) 1) 2`;;
val it : thm = |- (\x. (\y. y + x) 1) 2 = (\x. (\y. y + x) (SUC 0)) (SUC 1)
ONCE_DEPTH_CONV is frequently used when there is only one subterm to which
the desired conversion applies. This can be much faster than using other
functions that attempt to apply a conversion to all subterms of a term (e.g.
DEPTH_CONV). If, for example, the current goal in a goal-directed proof
contains only one beta-redex, and one wishes to apply BETA_CONV to it, then
may, depending on where the beta-redex occurs, be much faster than
CONV_TAC (ONCE_DEPTH_CONV BETA_CONV)
ONCE_DEPTH_CONV c may also be used when the supplied conversion c never
fails, in which case using a conversion such as DEPTH_CONV c, which
applies c repeatedly would never terminate.
CONV_TAC (TOP_DEPTH_CONV BETA_CONV)
- SEE ALSO
DEPTH_BINOP_CONV, DEPTH_CONV, PROP_ATOM_CONV, REDEPTH_CONV, TOP_DEPTH_CONV,