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
|
\DOC SUBST_MATCH
\TYPE {SUBST_MATCH : (thm -> thm -> thm)}
\SYNOPSIS
Substitutes in one theorem using another, equational, theorem.
\KEYWORDS
rule.
\DESCRIBE
Given the theorems {A|-u=v} and {A'|-t}, {SUBST_MATCH (A|-u=v) (A'|-t)}
searches for one free instance of {u} in {t}, according to a top-down
left-to-right search strategy, and then substitutes the corresponding instance
of {v}.
{
A |- u=v A' |- t
-------------------- SUBST_MATCH (A|-u=v) (A'|-t)
A u A' |- t[v/u]
}
\noindent {SUBST_MATCH} allows only a free instance of {u} to be substituted
for in {t}. An instance which contain bound variables can be substituted for by
using rewriting rules such as {REWRITE_RULE}, {PURE_REWRITE_RULE} and
{ONCE_REWRITE_RULE}.
\FAILURE
{SUBST_MATCH th1 th2} fails if the conclusion of the theorem {th1} is not an
equation. Moreover, {SUBST_MATCH (A|-u=v) (A'|-t)} fails if no instance of {u}
occurs in {t}, since the matching algorithm fails. No change is made to the
theorem {(A'|-t)} if instances of {u} occur in {t}, but they are not free (see
{SUBS}).
\EXAMPLE
The commutative law for addition
{
#let thm1 = SPECL ["m:num"; "n:num"] ADD_SYM;;
thm1 = |- m + n = n + m
}
\noindent is used to apply substitutions, depending on the occurrence of free
instances
{
#SUBST_MATCH thm1 (ASSUME "(n + 1) + (m - 1) = m + n");;
. |- (m - 1) + (n + 1) = m + n
#SUBST_MATCH thm1 (ASSUME "!n. (n + 1) + (m - 1) = m + n");;
. |- !n. (n + 1) + (m - 1) = m + n
}
\USES
{SUBST_MATCH} is used when rewriting with the rules such as {REWRITE_RULE},
using a single theorem is too extensive or would diverge. Moreover, applying
{SUBST_MATCH} can be much faster than using the rewriting rules.
\SEEALSO
ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE, SUBS, SUBST.
\ENDDOC
|
