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
|
\DOC PART_MATCH
\TYPE {PART_MATCH : ((term -> term) -> thm -> term -> thm)}
\SYNOPSIS
Instantiates a theorem by matching part of it to a term.
\KEYWORDS
rule.
\DESCRIBE
When applied to a `selector' function of type {term -> term}, a theorem and a
term:
{
PART_MATCH fn (A |- !x1...xn. t) tm
}
\noindent the function {PART_MATCH} applies {fn} to {t'} (the result of
specializing universally quantified variables in the conclusion of the
theorem), and attempts to match the resulting term to the argument term
{tm}. If it succeeds, the appropriately instantiated version of the
theorem is returned.
\FAILURE
Fails if the selector function {fn} fails when applied to the instantiated
theorem, or if the match fails with the term it has provided.
\EXAMPLE
Suppose that we have the following theorem:
{
th = |- !x. x==>x
}
\noindent then the following:
{
PART_MATCH (fst o dest_imp) th "T"
}
\noindent results in the theorem:
{
|- T ==> T
}
\noindent because the selector function picks the antecedent of the
implication (the inbuilt specialization gets rid of the universal
quantifier), and matches it to {T}.
\SEEALSO
INST_TYPE, INST_TY_TERM, match.
\ENDDOC
|
