BoundedRewrites.Once

STRUCTURE

SYNOPSIS

Rewriting control.

DESCRIPTION

When used as an argument to the rewriter or simplifier, Once th is a directive saying that th should be used at most once 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, the following invocation can be made

   - SIMP_CONV arith_ss [Once fact_def] ``fact 6``;
   > val it = |- fact 6 = 6 * fact 5 : thm

COMMENTS

Use of Once does not compose well. For example,

   tac1 THENL [SIMP_TAC std_ss [Once th],
               SIMP_TAC std_ss [Once th]]

is not equivalent in behaviour to

   tac1 THEN SIMP_TAC std_ss [Once th].

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

SEEALSO

Ntimes, THEN, SIMP_TAC, RW_TAC, ONCE_REWRITE_TAC