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
|
\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);;
val it : thm = |- !x. x ==> (!y. y ==> x)
# SPEC `~y` it;;
val it : thm = |- ~y ==> (!y'. y' ==> ~y)
}
\COMMENTS
In order to specialize variables while also instantiating types of polymorphic
variables, use {ISPEC} instead.
\SEEALSO
GEN, GENL, GEN_ALL, ISPEC, ISPECL, SPECL, SPEC_ALL, SPEC_VAR.
\ENDDOC
|
