1\DOC GEN_REWRITE_RULE
2
3\TYPE {GEN_REWRITE_RULE : ((conv -> conv) -> rewrites -> thm list -> thm -> thm)}
4
5\SYNOPSIS
6Rewrites a theorem, selecting terms according to a user-specified strategy.
7
8\KEYWORDS
9rule.
10
11\DESCRIBE
12Rewriting in HOL is based on the use of equational theorems as left-to-right
13replacements on the subterms of an object theorem.  This replacement is
14mediated by the use of {REWR_CONV}, which finds matches between left-hand
15sides of given equations in a term and applies the substitution.
16
17Equations used in rewriting are obtained from the theorem lists given as
18arguments to the function. These are at first transformed into a form suitable
19for rewriting. Conjunctions are separated into individual rewrites. Theorems
20with conclusions of the form {"~t"} are transformed into the corresponding
21equations {"t = F"}. Theorems {"t"} which are not equations are cast as
22equations of form {"t = T"}.
23
24If a theorem is used to rewrite the object theorem, its assumptions
25are added to the assumptions of the returned theorem, unless they are
26alpha-convertible to existing assumptions.  The matching involved uses
27variable instantiation. Thus, all free variables are generalized, and
28terms are instantiated before substitution. Theorems may have
29universally quantified variables.
30
31The theorems with which rewriting is done are divided
32into two groups, to facilitate implementing other rewriting tools.
33However, they are considered in an order-independent fashion. (That
34is, the ordering is an implementation detail which is not specified.)
35
36The search strategy for finding matching subterms is the first
37argument to the rule. Matching and substitution may occur at any
38level of the term, according to the specified search strategy: the
39whole term, or starting from any subterm. The search strategy also
40specifies the depth of the search: recursively up to an arbitrary
41depth until no matches occur, once over the selected subterm, or any
42more complex scheme.
43
44\FAILURE
45{GEN_REWRITE_RULE} fails if the search strategy fails. It may also
46cause a non-terminating sequence of rewrites, depending on the search
47strategy used.
48
49\USES
50This rule is used in the system to implement all other rewriting
51rules, and may provide a user with a method to fine-tune rewriting of
52theorems.
53
54\EXAMPLE
55Suppose we have a theorem of the form:
56{
57   thm = |- (1 + 2) + 3 = (3 + 1) + 2
58}
59and we would like to rewrite the left-hand side with the
60theorem {ADD_SYM} without changing the right hand side. This can be
61done by using:
62{
63   GEN_REWRITE_RULE (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [ADD_SYM] mythm
64}
65Other rules, such as {ONCE_REWRITE_RULE}, would match and
66substitute on both sides, which would not be the desirable result.
67
68As another example, {REWRITE_RULE} could be implemented as
69{
70    GEN_REWRITE_RULE TOP_DEPTH_CONV (implicit_rewrites())
71}
72which specifies that matches should be searched recursively
73starting from the whole term of the theorem, and {implicit_rewrites} must
74be added to the user defined set of theorems employed in rewriting.
75
76\SEEALSO
77Rewrite.ASM_REWRITE_RULE, Rewrite.FILTER_ASM_REWRITE_RULE, Rewrite.ONCE_REWRITE_RULE, Rewrite.PURE_REWRITE_RULE, Conv.REWR_CONV, Rewrite.REWRITE_RULE.
78\ENDDOC
79