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
|
\DOC GEN_PART_MATCH
\TYPE {GEN_PART_MATCH : (term -> term) -> thm -> term -> thm}
\SYNOPSIS
Instantiates a theorem by matching part of it to a term.
\DESCRIBE
When applied to a `selector' function of type {term -> term}, a theorem and a
term:
{
GEN_PART_MATCH fn (A |- !x1...xn. t) tm
}
\noindent the function {GEN_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. Limited higher-order matching is supported, and some
attempt is made to maintain bound variable names in higher-order matching.
Unlike {PART_MATCH}, free variables in the initial theorem that are
unconstrained by the instantiation will be renamed if necessary to avoid
clashes with determined free variables.
\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
See {MATCH_MP_TAC} for more basic examples. The following illustrates the
difference with that function
{
# let th = ARITH_RULE `m = n ==> m + p = n + p`;;
val th : thm = |- m = n ==> m + p = n + p
# PART_MATCH lhand th `n:num = p`;;
val it : thm = |- n = p ==> n + p = p + p
# GEN_PART_MATCH lhand th `n:num = p`;;
val it : thm = |- n = p ==> n + p' = p + p'
}
\SEEALSO
INST_TYPE, INST_TY_TERM, match, MATCH_MP, PART_MATCH, REWR_CONV.
\ENDDOC
|
