/usr/share/hol88-2.02.19940316/help/ENTRIES/SPECL.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 | \DOC SPECL
\TYPE {SPECL : (term list -> thm -> thm)}
\SYNOPSIS
Specializes zero or more variables in the conclusion of a theorem.
\KEYWORDS
rule.
\DESCRIBE
When applied to a term list {[u1;...;un]} and a theorem
{A |- !x1...xn. t}, the inference rule {SPECL} returns the theorem
{A |- t[u1/x1]...[un/xn]}, where the substitutions are made
sequentially left-to-right in the same way as for {SPEC}, with the same
sort of alpha-conversions applied to {t} if necessary to ensure that no
variables which are free in {ui} become bound after substitution.
{
A |- !x1...xn. t
-------------------------- SPECL "[u1;...;un]"
A |- t[u1/x1]...[un/xn]
}
\noindent It is permissible for the term-list to be empty, in which case
the application of {SPECL} has no effect.
\FAILURE
Fails unless each of the terms is of the same as that of the
appropriate quantified variable in the original theorem.
\EXAMPLE
The following is a specialization of a theorem from theory {arithmetic}.
{
#let t = theorem `arithmetic` `LESS_EQ_LESS_EQ_MONO`;;
t = |- !m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)
#SPECL ["1"; "2"; "3"; "4"] t;;
|- 1 <= 3 /\ 2 <= 4 ==> (1 + 2) <= (3 + 4)
}
\SEEALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPEC_ALL, SPEC_TAC.
\ENDDOC
|