Ntimes
BoundedRewrites.Ntimes : thm -> int -> thm
Rewriting control.
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.
See also
BoundedRewrites.Once,
Tactical.THEN,
simpLib.SIMP_TAC,
bossLib.RW_TAC,
Rewrite.REWRITE_TAC