ASM_REWRITE_TAC : thm list -> tactic

SYNOPSIS

Rewrites a goal including built-in rewrites and the goal's assumptions.

DESCRIPTION

ASM_REWRITE_TAC generates rewrites with the tautologies in basic_rewrites, the set of assumptions, and a list of theorems supplied by the user. These are applied top-down and recursively on the goal, until no more matches are found. The order in which the set of rewrite equations is applied is an implementation matter and the user should not depend on any ordering. Rewriting strategies are described in more detail under GEN_REWRITE_TAC. For omitting the common tautologies, see the tactic PURE_ASM_REWRITE_TAC.

FAILURE CONDITIONS

ASM_REWRITE_TAC does not fail, but it can diverge in certain situations. For rewriting to a limited depth, see ONCE_ASM_REWRITE_TAC. The resulting tactic may not be valid if the applicable replacement introduces new assumptions into the theorem eventually proved.

EXAMPLE

The use of assumptions in rewriting, specially when they are not in an obvious equational form, is illustrated below:

  # g `P ==> (P /\ Q /\ R <=> R /\ Q /\ P)`;;
  Warning: Free variables in goal: P, Q, R
  val it : goalstack = 1 subgoal (1 total)

  `P ==> (P /\ Q /\ R <=> R /\ Q /\ P)`

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

   0 [`P`]

  `P /\ Q /\ R <=> R /\ Q /\ P`

  # e(ASM_REWRITE_TAC[]);;
  val it : goalstack = 1 subgoal (1 total)

   0 [`P`]

  `Q /\ R <=> R /\ Q`