ONCE_REWRITE_TAC : thm list -> tactic

SYNOPSIS

Rewrites a goal only once with basic_rewrites and the supplied list of theorems.

DESCRIPTION

A set of equational rewrites is generated from the theorems supplied by the user and the set of basic tautologies, and these are used to rewrite the goal at all subterms at which a match is found in one pass over the term part of the goal. The result is returned without recursively applying the rewrite theorems to it. The order in which the given theorems are applied is an implementation matter and the user should not depend on any ordering. More details about rewriting can be found under GEN_REWRITE_TAC.

FAILURE CONDITIONS

ONCE_REWRITE_TAC does not fail and does not diverge. It results in an invalid tactic if any of the applied rewrites introduces new assumptions to the theorem eventually proved.

EXAMPLE

Given a theorem list:

  # let thl = map (num_CONV o mk_small_numeral) (1--3);;
  val thl : thm list = [|- 1 = SUC 0; |- 2 = SUC 1; |- 3 = SUC 2]

and the following goal:

  # g `0 < 3`;;
  val it : goalstack = 1 subgoal (1 total)

  `0 < 3`

the tactic ONCE_REWRITE_TAC thl performs a single rewrite

  # e(ONCE_REWRITE_TAC thl);;
  val it : goalstack = 1 subgoal (1 total)

  `0 < SUC 2`

in contrast to REWRITE_TAC thl which would rewrite the goal repeatedly into this form:

  # e(REWRITE_TAC thl);;
  val it : goalstack = 1 subgoal (1 total)

  `0 < SUC (SUC (SUC 0))`

USES

ONCE_REWRITE_TAC can be used iteratively to rewrite when recursive rewriting would diverge. It can also be used to save inference steps.