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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
\DOC REWR_CONV
\TYPE {REWR_CONV : thm -> term -> thm}
\SYNOPSIS
Uses an instance of a given equation to rewrite a term.
\KEYWORDS
conversion.
\DESCRIBE
{REWR_CONV} is one of the basic building blocks for the implementation of
rewriting in the HOL system. In particular, the term replacement or rewriting
done by all the built-in rewriting rules and tactics is ultimately done by
applications of {REWR_CONV} to appropriate subterms. The description given
here for {REWR_CONV} may therefore be taken as a specification of the atomic
action of replacing equals by equals that is used in all these higher level
rewriting tools.
The first argument to {REWR_CONV} is expected to be an equational theorem
which is to be used as a left-to-right rewrite rule. The general form of this
theorem is:
{
A |- t[x1,...,xn] = u[x1,...,xn]
}
\noindent where {x1}, ..., {xn} are all the variables that occur free in the
left-hand side of the conclusion of the theorem but do not occur free in the
assumptions. Any of these variables may also be universally quantified at the
outermost level of the equation, as for example in:
{
A |- !x1...xn. t[x1,...,xn] = u[x1,...,xn]
}
\noindent Note that {REWR_CONV} will also work, but will give a generally
undesirable result (see below), if the right-hand side of the equation contains
free variables that do not also occur free on the left-hand side, as for
example in:
{
A |- t[x1,...,xn] = u[x1,...,xn,y1,...,ym]
}
\noindent where the variables {y1}, ..., {ym} do not occur free in
{t[x1,...,xn]}.
If {th} is an equational theorem of the kind shown above, then
{REWR_CONV th} returns a conversion that maps terms of the form
{t[e1,...,en/x1,...,xn]}, in which the terms {e1}, ..., {en} are free for
{x1}, ..., {xn} in {t}, to theorems of the form:
{
A |- t[e1,...,en/x1,...,xn] = u[e1,...,en/x1,...,xn]
}
\noindent That is, {REWR_CONV th tm} attempts to match the left-hand side of
the rewrite rule {th} to the term {tm}. If such a match is possible, then
{REWR_CONV} returns the corresponding substitution instance of {th}.
If {REWR_CONV} is given a theorem {th}:
{
A |- t[x1,...,xn] = u[x1,...,xn,y1,...,ym]
}
\noindent where the variables {y1}, ..., {ym} do not occur free in the
left-hand side, then the result of applying the conversion {REWR_CONV th} to
a term {t[e1,...,en/x1,...,xn]} will be:
{
A |- t[e1,...,en/x1,...,xn] = u[e1,...,en,v1,...,vm/x1,...,xn,y1,...,ym]
}
\noindent where {v1}, ..., {vm} are variables chosen so as to be free nowhere
in {th} or in the input term. The user has no control over the choice of the
variables {v1}, ..., {vm}, and the variables actually chosen may well be
inconvenient for other purposes. This situation is, however, relatively rare;
in most equations the free variables on the right-hand side are a subset of the
free variables on the left-hand side.
In addition to doing substitution for free variables in the supplied equational
theorem (or `rewrite rule'), {REWR_CONV th tm} also does type instantiation,
if this is necessary in order to match the left-hand side of the given rewrite
rule {th} to the term argument {tm}. If, for example, {th} is the theorem:
{
A |- t[x1,...,xn] = u[x1,...,xn]
}
\noindent and the input term {tm} is (a substitution instance of) an instance
of {t[x1,...,xn]} in which the types {ty1}, ..., {tyi} are substituted for the
type variables {vty1}, ..., {vtyi}, that is if:
{
tm = t[ty1,...,tyn/vty1,...,vtyn][e1,...,en/x1,...,xn]
}
\noindent then {REWR_CONV th tm} returns:
{
A |- (t = u)[ty1,...,tyn/vty1,...,vtyn][e1,...,en/x1,...,xn]
}
\noindent Note that, in this case, the type variables {vty1}, ..., {vtyi} must
not occur anywhere in the hypotheses {A}. Otherwise, the conversion will fail.
\FAILURE
{REWR_CONV th} fails if {th} is not an equation or an equation universally
quantified at the outermost level. If {th} is such an equation:
{
th = A |- !v1....vi. t[x1,...,xn] = u[x1,...,xn,y1,...,yn]
}
\noindent then {REWR_CONV th tm} fails unless the term {tm} is
alpha-equivalent to an instance of the left-hand side {t[x1,...,xn]} which
can be obtained by instantiation of free type variables (i.e. type variables
not occurring in the assumptions {A}) and substitution for the free variables
{x1}, ..., {xn}.
\EXAMPLE
The following example illustrates a straightforward use of {REWR_CONV}.
The supplied rewrite rule is polymorphic, and both substitution for free
variables and type instantiation may take place. {EQ_SYM_EQ} is the theorem:
{
|- !x y:A. x = y <=> y = x
}
\noindent and {REWR_CONV EQ_SYM} behaves as follows:
{
# REWR_CONV EQ_SYM_EQ `1 = 2`;;
val it : thm = |- 1 = 2 <=> 2 = 1
# REWR_CONV EQ_SYM_EQ `1 < 2`;;
Exception: Failure "term_pmatch".
}
\noindent The second application fails because the left-hand side {`x = y`} of
the rewrite rule does not match the term to be rewritten, namely {`1 < 2`}.
In the following example, one might expect the result to be the theorem
{A |- f 2 = 2}, where {A} is the assumption of the supplied rewrite rule:
{
# REWR_CONV (ASSUME `!x:A. f x = x`) `f 2:num`;;
Exception: Failure "term_pmatch: can't instantiate local constant".
}
\noindent The application fails, however, because the type variable {A} appears
in the assumption of the theorem returned by {ASSUME `!x:A. f x = x`}.
Failure will also occur in situations like:
{
# REWR_CONV (ASSUME `f (n:num) = n`) `f 2:num`;;
Exception: Failure "term_pmatch: can't instantiate local constant".
}
\noindent where the left-hand side of the supplied equation contains a free
variable (in this case {n}) which is also free in the assumptions, but which
must be instantiated in order to match the input term.
\SEEALSO
IMP_REWR_CONV, ORDERED_REWR_CONV, REWRITE_CONV.
\ENDDOC
|
