Ntimes : thm -> int -> thm
STRUCTURE
SYNOPSIS
Rewriting control.
DESCRIPTION
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
HOL  Kananaskis-14