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
48
|
\DOC INST_TYPE
\TYPE {INST_TYPE : ((type # type) list -> thm -> thm)}
\SYNOPSIS
Instantiates types in a theorem.
\KEYWORDS
rule, type, instantiate.
\DESCRIBE
{INST_TYPE} is a primitive rule in the HOL logic, which allows
instantiation of type variables.
{
A |- t
----------------------------------- INST_TYPE [(ty1,vty1);...;(tyn,vtyn)]
A |- t[ty1,...,tyn/vty1,...,vtyn]
}
\noindent where none of the types {vtyi} are free in the assumption list.
Variables will be renamed if necessary to prevent distinct variables becoming
identical after the instantiation.
\FAILURE
{INST_TYPE} fails if any of the type variables occurs free in the
hypotheses of the theorem, or if upon instantiation two distinct
variables (with the same name) become equal.
\USES
{INST_TYPE} is employed to make use of polymorphic theorems.
\EXAMPLE
Suppose one wanted to specialize the theorem {EQ_SYM_EQ} for
particular values, the first attempt could be to use {SPECL} as
follows:
{
#SPECL ["a:num"; "b:num"] EQ_SYM_EQ ;;
evaluation failed SPECL
}
\noindent The failure occurred because {EQ_SYM_EQ} contains polymorphic types.
The desired specialization can be obtained by using {INST_TYPE}:
{
#SPECL ["a:num"; "b:num"] (INST_TYPE [":num",":*"] EQ_SYM_EQ) ;;
|- (a = b) = (b = a)
}
\SEEALSO
INST, INST_TY_TERM.
\ENDDOC
|
