INST : (term * term) list -> thm -> thm
Instantiates free variables in a theorem.
When INST [t1,x1; ...; tn,xn] is applied to a theorem, it gives a new
theorem that systematically replaces free instances of each variable xi with
the corresponding term ti in both assumptions and conclusion.
Bound variables will be renamed if necessary to avoid capture. All variables
are substituted in parallel, so there is no problem if there is an overlap
between the terms ti and xi.
A |- t
----------------------------------- INST_TYPE [t1,x1;...;tn,xn]
- FAILURE CONDITIONS
Fails if any of the pairs ti,xi in the instantiation list has xi and ti
with different types, or xi a non-variable. Multiple instances of the same
xi in the list are not trapped, but only the first one will be used
Here is a simple example
and here is one where bound variable renaming is needed.
# let th = SPEC_ALL ADD_SYM;;
val th : thm = |- m + n = n + m
# INST [`1`,`m:num`; `x:num`,`n:num`] th;;
val it : thm = |- 1 + x = x + 1
# let th = SPEC_ALL LE_EXISTS;;
val th : thm = |- m <= n <=> (?d. n = m + d)
# INST [`d:num`,`m:num`] th;;
val it : thm = |- d <= n <=> (?d'. n = d + d')
This is the most efficient way to obtain instances of a theorem; though
sometimes more convenient, SPEC and SPECL are significantly slower.
This is one of HOL Light's 10 primitive inference rules.
- SEE ALSO
INST_TYPE, ISPEC, ISPECL, SPEC, SPECL.