1\DOC SUBST
2
3\TYPE {SUBST : (term,thm) subst -> term -> thm -> thm}
4
5\SYNOPSIS
6Makes a set of parallel substitutions in a theorem.
7
8\KEYWORDS
9rule.
10
11\DESCRIBE
12Implements the following rule of simultaneous substitution
13{
14    A1 |- t1 = u1 ,  ... , An |- tn = un ,    A |- t[t1,...,tn]
15   -------------------------------------------------------------
16        A u A1 u ... u An |- t[u1,...,un]
17}
18Evaluating
19{
20   SUBST [x1 |-> (A1 |- t1=u1) ,..., xn |-> (An |- tn=un)]
21         t[x1,...,xn]
22         (A |- t[t1,...,tn])
23}
24returns the theorem {A u A1 u ... u An |- t[u1,...,un]} (perhaps with
25fewer assumptions, see paragraph below). The term argument {t[x1,...,xn]}
26is a template which should match the conclusion of the theorem being
27substituted into, with the variables {x1}, ... , {xn} marking those
28places where occurrences of {t1}, ... , {tn} are to be replaced by the
29terms {u1}, ... , {un}, respectively.  The occurrence of {ti} at the
30places marked by {xi} must be free (i.e. {ti} must not contain any bound
31variables).  {SUBST} automatically renames bound variables to prevent
32free variables in {ui} becoming bound after substitution.
33
34The assumptions of the returned theorem may not contain all the
35assumptions {A1 u ... u An} if some of them are not required. In
36particular, if the theorem {Ak |- tk = uk} is unnecessary because {xk}
37does not appear in the template, then {Ak} is not be added to the
38assumptions of the returned theorem.
39
40\FAILURE
41If the template does not match the conclusion of the hypothesis, or the
42terms in the conclusion marked by the variables {x1}, ... , {xn} in the
43template are not identical to the left hand sides of the supplied
44equations (i.e. the terms {t1}, ... , {tn}).
45
46\EXAMPLE
47{
48- val x = ���x:num���
49  and y = ���y:num���
50  and th0 = SPEC ���0��� arithmeticTheory.ADD1
51  and th1 = SPEC ���1��� arithmeticTheory.ADD1;
52
53(*    x = `x`
54      y = `y`
55    th0 = |- SUC 0 = 0 + 1
56    th1 = |- SUC 1 = 1 + 1     *)
57
58- SUBST [x |-> th0, y |-> th1]
59        ���(x+y) > SUC 0���
60        (ASSUME ���(SUC 0 + SUC 1) > SUC 0���);
61
62> val it = [.] |- (0 + 1) + 1 + 1 > SUC 0 : thm
63
64
65- SUBST [x |-> th0, y |-> th1]
66        ���(SUC 0 + y) > SUC 0���
67        (ASSUME ���(SUC 0 + SUC 1) > SUC 0���);
68
69> val it = [.] |- SUC 0 + 1 + 1 > SUC 0 : thm
70
71
72- SUBST [x |-> th0, y |-> th1]
73        ���(x+y) > x���
74        (ASSUME ���(SUC 0 + SUC 1) > SUC 0���);
75
76> val it = [.] |- (0 + 1) + 1 + 1 > 0 + 1 : thm
77}
78
79
80\COMMENTS
81{SUBST} is perhaps overly complex for a primitive rule of inference.
82
83\USES
84For substituting at selected occurrences. Often useful for writing
85special purpose derived inference rules.
86
87\SEEALSO
88Drule.SUBS, Drule.SUBST_CONV, Lib.|->.
89\ENDDOC
90