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
|
\DOC PART_PMATCH
\TYPE {PART_PMATCH : ((term -> term) -> thm -> term -> thm)}
\SYNOPSIS
Instantiates a theorem by matching part of it to a term.
\KEYWORDS
rule.
\LIBRARY pair
\DESCRIBE
When applied to a `selector' function of type {term -> term}, a theorem and a
term:
{
PART_MATCH fn (A |- !p1...pn. t) tm
}
\noindent the function {PART_PMATCH} applies {fn} to {t'} (the result
of specializing universally quantified pairs 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.
\SEEALSO
PART_MATCH.
\ENDDOC
|
