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
|
\DOC ISPEC
\TYPE {ISPEC : term -> thm -> thm}
\SYNOPSIS
Specializes a theorem, with type instantiation if necessary.
\KEYWORDS
rule, type.
\DESCRIBE
This rule specializes a quantified variable as does {SPEC}; it differs
from it in also instantiating the type if needed, both in the conclusion and
hypotheses:
{
A |- !x:ty.tm
----------------------- ISPEC `t:ty'`
A[ty'/ty] |- tm[t/x]
}
\noindent (where {t} is free for {x} in {tm}, and {ty'} is an instance
of {ty}).
\FAILURE
{ISPEC} fails if the input theorem is not universally quantified, or if
the type of the given term is not an instance of the type of the
quantified variable.
\EXAMPLE
{
# ISPEC `0` EQ_REFL;;
val it : thm = |- 0 = 0
}
\noindent Note that the corresponding call to {SPEC} would fail because of the
type mismatch:
{
# SPEC `0` EQ_REFL;;
Exception: Failure "SPEC".
}
\SEEALSO
INST, INST_TYPE, ISPECL, SPEC, type_match.
\ENDDOC
|
