`TOP_DEPTH_CONV : conv -> conv`

SYNOPSIS
Applies a conversion top-down to all subterms, retraversing changed ones.

DESCRIPTION
TOP_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 c is applied to the subterms of tm in top-down order and is applied repeatedly (zero or more times, as is done by REPEATC) at each subterm until it fails. If a subterm t is changed (except for alpha-equivalence) by virtue of the application of c to its own subterms, then the term into which t is transformed is retraversed by applying TOP_DEPTH_CONV c to it.

FAILURE CONDITIONS
TOP_DEPTH_CONV c tm never fails but can diverge.

EXAMPLE
Both TOP_DEPTH_CONV and REDEPTH_CONV repeatedly apply a conversion until no more applications are possible anywhere in the term. For example, TOP_DEPTH_CONV BETA_CONV or REDEPTH_CONV BETA_CONV will eliminate all beta redexes:
```  # TOP_DEPTH_CONV BETA_CONV `(\x. (\y. (\z. z + y) (y + 1)) (x + 2)) 3`;;
val it : thm =
|- (\x. (\y. (\z. z + y) (y + 1)) (x + 2)) 3 = ((3 + 2) + 1) + 3 + 2
```
The main difference is that TOP_DEPTH_CONV proceeds top-down, whereas REDEPTH_CONV proceeds bottom-up. Reasons for preferring TOP_DEPTH_CONV might be that a transformation near the top obviates the need for transformations lower down. For example, this is quick because everything is done by one top-level rewrite:
```  # let conv = GEN_REWRITE_CONV I [MULT_CLAUSES] ORELSEC NUM_RED_CONV;;
val conv : conv =

# time (TOP_DEPTH_CONV conv) `0 * 25 EXP 100`;;
CPU time (user): 0.
val it : thm = |- 0 * 25 EXP 100 = 0
```
whereas the following takes markedly longer:
```  # time (REDEPTH_CONV conv) `0 * 25 EXP 100`;;
CPU time (user): 2.573
val it : thm = |- 0 * 25 EXP 100 = 0
```