Applies a conversion bottom-up to all subterms, retraversing changed ones.
DESCRIPTION
REDEPTH_CONV c tm applies the conversion c repeatedly to all subterms of
the term tm and recursively applies REDEPTH_CONV c to each subterm at which
c succeeds, until there is no subterm remaining for which application of c
succeeds.
More precisely, REDEPTH_CONV c tm repeatedly applies the conversion c to
all the subterms of the term tm, including the term tm itself. The supplied
conversion c is applied to the subterms of tm in bottom-up order and is
applied repeatedly (zero or more times, as is done by REPEATC) to each
subterm until it fails. If c is successfully applied at least once to a
subterm, t say, then the term into which t is transformed is retraversed by
applying REDEPTH_CONV c to it.
FAILURE CONDITIONS
REDEPTH_CONV c tm never fails but can diverge if the conversion c can be
applied repeatedly to some subterm of tm without failing.
EXAMPLE
The following example shows how REDEPTH_CONV retraverses subterms:
# REDEPTH_CONV BETA_CONV `(\f x. (f x) + 1) (\y.y) 2`;;
val it : thm = |- (\f x. f x + 1) (\y. y) 2 = 2 + 1
Here, BETA_CONV is first applied successfully to the (beta-redex)
subterm:
`(\f x. (f x) + 1) (\y.y)`
This application reduces this subterm to:
`(\x. ((\y.y) x) + 1)`
REDEPTH_CONV BETA_CONV is then recursively applied to this
transformed subterm, eventually reducing it to `(\x. x + 1)`. Finally, a
beta-reduction of the top-level term, now the simplified beta-redex
`(\x. x + 1) 2`, produces `2 + 1`.