Once : thm -> thm
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
HOL  Kananaskis-14