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