/usr/share/hol88-2.02.19940316/help/ENTRIES/SUBST.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | \DOC SUBST
\TYPE {SUBST : ((thm # term) list -> term -> thm -> thm)}
\SYNOPSIS
Makes a set of parallel substitutions in a theorem.
\KEYWORDS
rule.
\DESCRIBE
Implements the following rule of simultaneous substitution
{
A1 |- t1 = u1 , ... , An |- tn = un , A |- t[t1,...,tn]
-------------------------------------------------------------
A u A1 u ... u An |- t[ui]
}
\noindent Evaluating
{
SUBST [((A1 |- t1=u1), x1); ... ;((An |- tn=un), xn)]
t[x1,...,xn]
(A |- t[t1,...,tn])
}
\noindent returns the theorem {A |- t[u1,...,un]}. The term argument
{t[x1,...,xn]} is a template which should match the conclusion of the theorem
being substituted into, with the variables {x1}, ... , {xn} marking those
places where occurrences of {t1}, ... , {tn} are to be replaced by the terms
{u1}, ... , {un}, respectively. The occurrence of {ti} at the places marked by
{xi} must be free (i.e. {ti} must not contain any bound variables). {SUBST}
automatically renames bound variables to prevent free variables in {ui}
becoming bound after substitution.
{SUBST} is a complex primitive because it performs both parallel simultaneous
substitution and renaming of variables. This is for efficiency reasons, but it
would be logically cleaner if {SUBST} were simpler.
\FAILURE
If the template does not match the conclusion of the hypothesis, or the terms
in the conclusion marked by the variables {x1}, ... , {xn} in the template are
not identical to the left hand sides of the supplied equations (i.e. the terms
{t1}, ... , {tn}).
\EXAMPLE
{
#let th0 = SPEC "0" ADD1 and th1 = SPEC "1" ADD1;;
th0 = |- SUC 0 = 0 + 1
th1 = |- SUC 1 = 1 + 1
#SUBST [(th0,"x:num");(th1,"y:num")]
# "(x+y) > SUC 0"
# (ASSUME "(SUC 0 + SUC 1) > SUC 0");;
. |- ((0 + 1) + (1 + 1)) > (SUC 0)
#SUBST [(th0,"x:num");(th1,"y:num")]
# "(SUC 0 + y) > SUC 0"
# (ASSUME "(SUC 0 + SUC 1) > SUC 0");;
. |- ((SUC 0) + (1 + 1)) > (SUC 0)
#SUBST [(th0,"x:num");(th1,"y:num")]
# "(x+y) > x"
# (ASSUME "(SUC 0 + SUC 1) > SUC 0");;
. |- ((0 + 1) + (1 + 1)) > (0 + 1)
}
\USES
For substituting at selected occurrences. Often useful
for writing special purpose derived inference rules.
\SEEALSO
SUBS.
\ENDDOC
|