/usr/share/hol88-2.02.19940316/help/ENTRIES/SPEC.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 | \DOC SPEC
\TYPE {SPEC : (term -> thm -> thm)}
\SYNOPSIS
Specializes the conclusion of a theorem.
\KEYWORDS
rule.
\DESCRIBE
When applied to a term {u} and a theorem {A |- !x. t}, then {SPEC} returns
the theorem {A |- t[u/x]}. If necessary, variables will be renamed prior
to the specialization to ensure that {u} is free for {x} in {t}, that is,
no variables free in {u} become bound after substitution.
{
A |- !x. t
-------------- SPEC "u"
A |- t[u/x]
}
\FAILURE
Fails if the theorem's conclusion is not universally quantified, or if {x} and
{u} have different types.
\EXAMPLE
The following example shows how {SPEC} renames bound variables if necessary,
prior to substitution: a straightforward substitution would result in the
clearly invalid theorem {|- ~y ==> (!y. y ==> ~y)}.
{
#let xv = "x:bool" and yv="y:bool" in
# (GEN xv o DISCH xv o GEN yv o DISCH yv) (ASSUME xv);;
|- !x. x ==> (!y. y ==> x)
#SPEC "~y" it;;
|- ~y ==> (!y'. y' ==> ~y)
}
\SEEALSO
ISPEC, SPECL, SPEC_ALL, SPEC_VAR, GEN, GENL, GEN_ALL.
\ENDDOC
|