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
|
\DOC INST
\TYPE {INST : ((term # term) list -> thm -> thm)}
\SYNOPSIS
Instantiates free variables in a theorem.
\KEYWORDS
rule, instantiate.
\DESCRIBE
{INST} is a rule for substituting arbitrary terms for free variables
in a theorem:
{
A |- t
----------------------------- INST [(t1,x1);...;(tn,xn)]
A |- t[t1,...,tn/x1,...,xn]
}
\noindent where the variables {x1, ..., xn} are not free in the
assumptions {A}.
\FAILURE
{INST} fails if a variable being instantiated is free in the
assumptions.
\EXAMPLE
In the following example a theorem is instantiated for a specific term:
{
#CONJUNCT1 ADD_CLAUSES ;;
|- 0 + m = m
#INST [("2 * x","m:num")] (CONJUNCT1 ADD_CLAUSES) ;;
|- 0 + (2 * x) = 2 * x
}
\SEEALSO
INST_TY_TERM, INST_TYPE, ISPEC, ISPECL, SPEC; SPECL, SUBS, subst, SUBST.
\ENDDOC
|
