BoundedRewrites.Ntimes

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

Once, THEN, SIMP_TAC, RW_TAC, REWRITE_TAC