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
|
\DOC SUBST_CONV
\TYPE {SUBST_CONV : ((thm # term) list -> term -> conv)}
\SYNOPSIS
Makes substitutions in a term at selected occurrences of subterms, using a list
of theorems.
\KEYWORDS
conversion.
\DESCRIBE
{SUBST_CONV} implements the following rule of simultaneous substitution
{
A1 |- t1 = v1 ... An |- tn = vn
------------------------------------------------------------------
A1 u ... u An |- t[t1,...,tn/x1,...,xn] = t[v1,...,vn/x1,...,xn]
}
\noindent The first argument to {SUBST_CONV} is a list
{[(A1|-t1=v1, x1);...;(An|-tn=vn, xn)]}.
The second argument is a template term {t[x1,...,xn]}, in which
the variables {x1,...,xn} are used to mark those places where
occurrences of {t1,...,tn} are to be replaced with the terms
{v1,...,vn}, respectively.
Thus, evaluating
{
SUBST_CONV [(A1|-t1=v1, x1);...;(An|-tn=vn, xn)]
t[x1,...,xn]
t[t1,...,tn/x1,...,xn]
}
\noindent returns the theorem
{
A1 u ... u An |- t[t1,...,tn/x1,...,xn] = t[v1,...,vn/x1,...,xn]
}
The occurrence of {ti} at the places marked by the variable
{xi} must be free (i.e. {ti} must not contain any bound variables).
{SUBST_CONV} automatically renames bound variables to prevent free
variables in {vi} becoming bound after substitution.
\FAILURE
{SUBST_CONV [(th1,x1);...;(thn,xn)] t[x1,...,xn] t'} fails if the conclusion of
any theorem {thi} in the list is not an equation; or if the template
{t[x1,...,xn]} does not match the term {t'}; or if and term {ti} in {t'}
marked by the variable {xi} in the template, is not identical to the left-hand
side of the conclusion of the theorem {thi}.
\EXAMPLE
The theorems
{
#let thm0 = SPEC "0" ADD1 and thm1 = SPEC "1" ADD1;;
thm0 = |- SUC 0 = 0 + 1
thm1 = |- SUC 1 = 1 + 1
}
\noindent can be used to substitute selected occurrences of the terms {SUC 0}
and {SUC 1}
{
#SUBST_CONV [(thm0,"x:num");(thm1,"y:num")]
# "(x + y) > SUC 1"
# "(SUC 0 + SUC 1) > SUC 1";;
|- ((SUC 0) + (SUC 1)) > (SUC 1) = ((0 + 1) + (1 + 1)) > (SUC 1)
}
\USES
{SUBST_CONV} is used when substituting at selected occurrences of terms
and using rewriting rules/conversions is too extensive.
\SEEALSO
REWR_CONV, SUBS, SUBST, SUBS_OCCS.
\ENDDOC
|
