INST_TYPE
Thm.INST_TYPE : (hol_type,hol_type) subst -> thm -> thm
Instantiates types in a theorem.
INST_TYPE is a primitive rule in the HOL logic, which allows
instantiation of type variables.
A |- t
----------------------------------- INST_TYPE[vty1|->ty1,..., vtyn|->tyn]
A[ty1,...,tyn/vty1,...,vtyn]
|-
t[ty1,...,tyn/vty1,...,vtyn]
Type substitution is performed throughout the hypotheses and the conclusion. Variables will be renamed if necessary to prevent distinct bound variables becoming identical after the instantiation.
Failure
Never fails.
INST_TYPE enables polymorphic theorems to be used at any type.
Example
Supposing 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;
uncaught exception HOL_ERR
The failure occurred because EQ_SYM_EQ contains polymorphic types. The
desired specialization can be obtained by using INST_TYPE:
- load "numTheory";
- SPECL [Term `a:num`, Term`b:num`]
(INST_TYPE [alpha |-> Type`:num`] EQ_SYM_EQ);
> val it = |- (a = b) = (b = a) : thm