GEN_PART_MATCH : (term -> term) -> thm -> term -> thm
Instantiates a theorem by matching part of it to a term.
When applied to a `selector' function of type term -> term, a theorem and a
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.
GEN_PART_MATCH fn (A |- !x1...xn. t) tm
- FAILURE CONDITIONS
Fails if the selector function fn fails when applied to the instantiated
theorem, or if the match fails with the term it has provided.
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'
- SEE ALSO
INST_TYPE, INST_TY_TERM, MATCH_MP, PART_MATCH, REWR_CONV, term_match.