1\DOC GEN_REWRITE_TAC
2
3\TYPE {GEN_REWRITE_TAC : ((conv -> conv) -> rewrites -> thm list -> tactic)}
4
5\SYNOPSIS
6Rewrites a goal, selecting terms according to a user-specified strategy.
7
8\KEYWORDS
9tactic.
10
11\DESCRIBE
12Distinct rewriting tactics differ in the search strategies used in
13finding subterms on which to apply substitutions, and the
14built-in theorems used in rewriting. In the case of {REWRITE_TAC},
15this is a recursive traversal starting from the body of the goal's
16conclusion part, while in the case of {ONCE_REWRITE_TAC}, for example,
17the search stops as soon as a term on which a substitution is possible
18is found. {GEN_REWRITE_TAC} allows a user to specify a more complex
19strategy for rewriting.
20
21The basis of pattern-matching for rewriting is the notion of
22conversions, through the application of {REWR_CONV}.  Conversions
23are rules for mapping terms with theorems equating the given terms to
24other semantically equivalent ones.
25
26When attempting to rewrite subterms recursively, the use of
27conversions (and therefore rewrites) can be automated further by using
28functions which take a conversion and search for instances at which
29they are applicable. Examples of these functions are {ONCE_DEPTH_CONV}
30and {RAND_CONV}. The first argument to {GEN_REWRITE_TAC} is such a
31function, which specifies a search strategy; i.e. it specifies how
32subterms (on which substitutions are allowed) should be searched for.
33
34The second and third arguments are lists of theorems used for
35rewriting. The order in which these are used is not specified. The
36theorems need not be in equational form: negated terms, say {"~ t"},
37are transformed into the equivalent equational form {"t = F"}, while
38other non-equational theorems with conclusion of form {"t"} are cast
39as the corresponding equations {"t = T"}. Conjunctions are separated
40into the individual components, which are used as distinct rewrites.
41
42\FAILURE
43{GEN_REWRITE_TAC} fails if the search strategy fails. It may also
44cause a non-terminating sequence of rewrites, depending on the search
45strategy used. The resulting tactic is invalid when a theorem which
46matches the goal (and which is thus used for rewriting it with) has a
47hypothesis which is not alpha-convertible to any of the assumptions of
48the goal. Applying such an invalid tactic may result in a proof of
49a theorem which does not correspond to the original goal.
50
51\USES
52Detailed control of rewriting strategy, allowing a user to specify a
53search strategy.
54
55\EXAMPLE
56Given a goal such as:
57{
58   ?- a - (b + c) = a - (c + b)
59}
60we may want to rewrite only one side of it with a theorem,
61say {ADD_SYM}. Rewriting tactics which operate recursively result in
62divergence; the tactic {ONCE_REWRITE_TAC [ADD_SYM]} rewrites on both
63sides to produce the following goal:
64{
65   ?- a - (c + b) = a - (b + c)
66}
67as {ADD_SYM} matches at two positions. To rewrite on
68only one side of the equation, the following tactic can be used:
69{
70   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [ADD_SYM]
71}
72which produces the desired goal:
73{
74   ?- a - (c + b) = a - (c + b)
75}
76
77As another example, one can write a tactic which will behave similarly
78to {REWRITE_TAC} but will also include {ADD_CLAUSES} in the set of
79theorems to use always:
80{
81   val ADD_REWRITE_TAC = GEN_REWRITE_TAC TOP_DEPTH_CONV
82                             (add_rewrites (implicit_rewrites ())
83                                           [ADD_CLAUSES])
84}
85
86
87\SEEALSO
88Rewrite.ASM_REWRITE_TAC, Rewrite.GEN_REWRITE_RULE, Rewrite.ONCE_REWRITE_TAC, Rewrite.PURE_REWRITE_TAC, Conv.REWR_CONV, Rewrite.REWRITE_TAC.
89\ENDDOC
90