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
|
\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 = ARITH_RULE `!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)`;;
val t : thm = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q
# SPECL [`1`; `2`; `3`; `4`] t;;;
val it : thm = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4
}
\COMMENTS
In order to specialize variables while also instantiating types of polymorphic
variables, use {ISPECL} instead.
\SEEALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPEC_ALL, SPEC_TAC.
\ENDDOC
|
