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 ISPECL
\TYPE {ISPECL : term list -> thm -> thm}
\SYNOPSIS
Specializes a theorem zero or more times, with type instantiation if necessary.
\KEYWORDS
rule, type.
\DESCRIBE
{ISPECL} is an iterative version of {ISPEC}
{
A |- !x1...xn.t
----------------------------- ISPECL [`t1`,...,`tn`]
A' |- t[t1,...tn/x1,...,xn]
}
\noindent (where {ti} is free for {xi} in {tm}) in which {A'} results from
applying all the corresponding type instantiations to the assumption list {A}.
\FAILURE
{ISPECL} fails if the list of terms is longer than the number of
quantified variables in the term, or if the type instantiation fails.
\EXAMPLE
{
# ISPECL [`x:num`; `2`] EQ_SYM_EQ;;
val it : thm = |- x = 2 <=> 2 = x
}
\noindent Note that the corresponding call to {SPECL} would fail because of the
type mismatch:
{
# SPECL [`x:num`; `2`] EQ_SYM_EQ;;
Exception: Failure "SPECL".
}
\SEEALSO
INST_TYPE, INST, ISPEC, SPEC, SPECL, type_match.
\ENDDOC
|
