1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
\DOC REWRITE_CONV
\TYPE {REWRITE_CONV : (thm list -> conv)}
\SYNOPSIS
Rewrites a term including built-in tautologies in the list of rewrites.
\KEYWORDS
conversion.
\DESCRIBE
Rewriting a term using {REWRITE_CONV} utilizes as rewrites two sets
of theorems: the tautologies in the ML list {basic_rewrites} and the
ones supplied by the user. The rule searches top-down and recursively
for subterms which match the left-hand side of any of the possible
rewrites, until none of the transformations are applicable. There is no
ordering specified among the set of rewrites.
Variants of this conversion allow changes in the set of equations used:
{PURE_REWRITE_CONV} and others in its family do not rewrite with the
theorems in {basic_rewrites}.
The top-down recursive search for matches may not be desirable, as
this may increase the number of inferences being made or may result in
divergence. In this case other rewriting tools such as
{ONCE_REWRITE_CONV} and {GEN_REWRITE_CONV} can be used, or the set of
theorems given may be reduced.
See {GEN_REWRITE_CONV} for the general strategy for simplifying
theorems in HOL using equational theorems.
\FAILURE
Does not fail, but may diverge if the sequence of rewrites is
non-terminating.
\USES
Used to manipulate terms by rewriting them with theorems.
While resulting in high degree of automation, {REWRITE_CONV} can
spawn a large number of inference steps. Thus, variants such
as {PURE_REWRITE_CONV}, or other rules such as {SUBST_CONV}, may be used
instead to improve efficiency.
\SEEALSO
basic_rewrites, GEN_REWRITE_CONV, ONCE_REWRITE_CONV,
PURE_REWRITE_CONV, REWR_CONV, SUBST_CONV.
\ENDDOC
|
