1\DOC REWRITE_TAC
2
3\TYPE {REWRITE_TAC : (thm list -> tactic)}
4
5\SYNOPSIS
6Rewrites a goal including built-in tautologies in the list of rewrites.
7
8\KEYWORDS
9tactic.
10
11\DESCRIBE
12Rewriting tactics in HOL provide a recursive left-to-right matching
13and rewriting facility that automatically decomposes subgoals and
14justifies segments of proof in which equational theorems are used,
15singly or collectively.  These include the unfolding of definitions,
16and the substitution of equals for equals.  Rewriting is used either
17to advance or to complete the decomposition of subgoals.
18
19{REWRITE_TAC} transforms (or solves) a goal by using as rewrite rules
20(i.e. as left-to-right replacement rules) the conclusions of the given
21list of (equational) theorems, as well as a set of built-in theorems
22(common tautologies) held in the ML variable {implicit_rewrites}.
23Recognition of a tautology often terminates the subgoaling process
24(i.e. solves the goal).
25
26The equational rewrites generated are applied recursively and to
27arbitrary depth, with matching and instantiation of variables and type
28variables.  A list of rewrites can set off an infinite rewriting
29process, and it is not, of course, decidable in general whether a
30rewrite set has that property. The order in which the rewrite theorems
31are applied is unspecified, and the user should not depend on any
32ordering.
33
34See {GEN_REWRITE_TAC} for more details on the rewriting process.
35Variants of {REWRITE_TAC} allow the use of a different set of
36rewrites. Some of them, such as {PURE_REWRITE_TAC}, exclude the basic
37tautologies from the possible transformations. {ASM_REWRITE_TAC} and
38others include the assumptions at the goal in the set of possible
39rewrites.
40
41Still other tactics allow greater control over the search for
42rewritable subterms. Several of them such as {ONCE_REWRITE_TAC} do not
43apply rewrites recursively. {GEN_REWRITE_TAC} allows a rewrite to be
44applied at a particular subterm.
45
46\FAILURE
47{REWRITE_TAC} does not fail. Certain sets of rewriting theorems on
48certain goals may cause a non-terminating sequence of rewrites.
49Divergent rewriting behaviour results from a term {t} being
50immediately or eventually rewritten to a term containing {t} as a
51sub-term. The exact behaviour depends on the {HOL} implementation.
52
53\EXAMPLE
54The arithmetic theorem {GREATER_DEF}, {|- !m n. m > n = n < m}, is used
55below to advance a goal:
56{
57   - REWRITE_TAC [GREATER_DEF] ([],``5 > 4``);
58   > ([([], ``4 < 5``)], -) : subgoals
59}
60It is used below with the theorem {LESS_0},
61{|- !n. 0 < (SUC n)}, to solve a goal:
62{
63   - val (gl,p) =
64       REWRITE_TAC [GREATER_DEF, LESS_0] ([],``(SUC n) > 0``);
65   > val gl = [] : goal list
66   > val p = fn : proof
67
68   - p[];
69   > val it = |- (SUC n) > 0 : thm
70}
71
72
73\USES
74Rewriting is a powerful and general mechanism in HOL, and an important
75part of many proofs.  It relieves the user of the burden of directing
76and justifying a large number of minor proof steps.  {REWRITE_TAC}
77fits a forward proof sequence smoothly into the general goal-oriented
78framework. That is, (within one subgoaling step) it produces and
79justifies certain forward inferences, none of which are necessarily on
80a direct path to the desired goal.
81
82{REWRITE_TAC} may be more powerful a tactic than is needed in certain
83situations; if efficiency is at stake, alternatives might be
84considered.  On the other hand, if more power is required, the
85simplification functions ({SIMP_TAC} and others) may be appropriate.
86
87\SEEALSO
88Rewrite.ASM_REWRITE_TAC, Rewrite.GEN_REWRITE_TAC, Rewrite.FILTER_ASM_REWRITE_TAC, Rewrite.FILTER_ONCE_ASM_REWRITE_TAC, Rewrite.ONCE_ASM_REWRITE_TAC, Rewrite.ONCE_REWRITE_TAC, Rewrite.PURE_ASM_REWRITE_TAC, Rewrite.PURE_ONCE_ASM_REWRITE_TAC, Rewrite.PURE_ONCE_REWRITE_TAC, Rewrite.PURE_REWRITE_TAC, Conv.REWR_CONV, Rewrite.REWRITE_CONV, simpLib.SIMP_TAC, Tactic.SUBST_TAC.
89\ENDDOC
90