ONCE_DEPTH_CONV : conv -> conv

SYNOPSIS

Applies a conversion once to the first suitable sub-term(s) encountered in top-down order.

DESCRIPTION

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

Never fails.

EXAMPLE

The following example shows how ONCE_DEPTH_CONV applies a conversion to only the first suitable subterm(s) found in a top-down search:

  # 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, 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 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)

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.

USES

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 the tactic

   CONV_TAC (ONCE_DEPTH_CONV BETA_CONV)

may, depending on where the beta-redex occurs, be much faster than

   CONV_TAC (TOP_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.