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