/usr/share/hol88-2.02.19940316/help/ENTRIES/SUBS.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 | \DOC SUBS
\TYPE {SUBS : (thm list -> thm -> thm)}
\SYNOPSIS
Makes simple term substitutions in a theorem using a given list of theorems.
\KEYWORDS
rule.
\DESCRIBE
Term substitution in HOL is performed by replacing free subterms according to
the transformations specified by a list of equational theorems. Given a list
of theorems {A1|-t1=v1,...,An|-tn=vn} and a theorem {A|-t}, {SUBS}
simultaneously replaces each free occurrence of {ti} in {t} with {vi}:
{
A1|-t1=v1 ... An|-tn=vn A|-t
--------------------------------------------- SUBS[A1|-t1=v1;...;An|-tn=vn]
A1 u ... u An u A |- t[v1,...,vn/t1,...,tn] (A|-t)
}
\noindent No matching is involved; the occurrence of each {ti} being
substituted for must be a free in {t} (see {SUBST_MATCH}). An occurrence which
is not free can be substituted by using rewriting rules such as {REWRITE_RULE},
{PURE_REWRITE_RULE} and {ONCE_REWRITE_RULE}.
\FAILURE
{SUBS [th1;...;thn] (A|-t)} fails if the conclusion of each theorem in the list
is not an equation. No change is made to the theorem {A |- t} if no occurrence
of any left-hand side of the supplied equations appears in {t}.
\EXAMPLE
Substitutions are made with the theorems
{
#let thm1 = SPECL ["m:num"; "n:num"] ADD_SYM
#and thm2 = CONJUNCT1 ADD_CLAUSES;;
thm1 = |- m + n = n + m
thm2 = |- 0 + m = m
}
\noindent depending on the occurrence of free subterms
{
#SUBS [thm1; thm2] (ASSUME "(n + 0) + (0 + m) = m + n");;
. |- (n + 0) + m = n + m
#SUBS [thm1; thm2] (ASSUME "!n. (n + 0) + (0 + m) = m + n");;
. |- !n. (n + 0) + m = m + n
}
\USES
{SUBS} can sometimes be used when rewriting (for example, with {REWRITE_RULE})
would diverge and term instantiation is not needed. Moreover, applying the
substitution rules is often much faster than using the rewriting rules.
\SEEALSO
ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE, SUBST, SUBST_MATCH,
SUBS_OCCS.
\ENDDOC
|