----------------------------------------------------------------------
Ntimes                                               (BoundedRewrites)
----------------------------------------------------------------------
Ntimes : thm -> int -> thm

SYNOPSIS
Rewriting control.

KEYWORDS
Rewriting, simplification.

DESCRIBE
When used as an argument to the rewriter or simplifier, {Ntimes th n} is
a directive saying that {th} should be used at most {n} times in the
rewriting process. This is useful for controlling looping rewrites.

FAILURE
Never fails.

EXAMPLE
Suppose factorial was defined as follows:

   - val fact_def = Define `fact n = if n=0 then 1 else n * fact (n-1)`;
   Equations stored under "fact_def".
   Induction stored under "fact_ind".
   > val fact_def = |- fact n = (if n = 0 then 1 else n * fact (n - 1)) : thm

The theorem {fact_def} is a looping rewrite since the recursive call
{fac (n-1)} matches the left-hand side of {fact_def}. Thus, a naive
application of the simplifier will loop:

   - SIMP_CONV arith_ss [fact_def] ``fact 6``;
   (* looping *)
   > Interrupted.

In order to expand the definition of {fact_def} three times, the
following invocation can be made

   - SIMP_CONV arith_ss [Ntimes Fact_def 3] ``fact 6``;
   > val it = |- fact 6 = 6 * (5 * (4 * fact 3)) : thm


COMMENTS
Use of {Ntimes} does not compose well. For example,

   tac1 THENL [SIMP_TAC std_ss [Ntimes th 1],
               SIMP_TAC std_ss [Ntimes th 1]]

is not equivalent in behaviour to

   tac1 THEN SIMP_TAC std_ss [Ntimes th 1].

In the first call two rewrites using {th} can occur; in the second,
only one can occur.

SEEALSO
BoundedRewrites.Once, Tactical.THEN, simpLib.SIMP_TAC, bossLib.RW_TAC,
Rewrite.REWRITE_TAC.

----------------------------------------------------------------------