PART_MATCH
Drule.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 term:
PART_MATCH fn (A |- !x1...xn. t) tm
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.
Since PART_MATCH will not instantiate variables which appear in the
hypotheses of the given theorem, it fails if the attempted match would
require instantiating these variables. To allow instantiation of these
variables, use PART_MATCH_A.
Example
Suppose that we have the following theorem:
th = |- !x. x==>x
then the following:
PART_MATCH (fst o dest_imp) th "T"
results in the theorem:
|- T ==> T
because the selector function picks the antecedent of the implication
(the inbuilt specialization gets rid of the universal quantifier), and
matches it to T.
See also
Drule.PART_MATCH',
Drule.PART_MATCH_A,
Thm.INST_TYPE,
Drule.INST_TY_TERM,
Term.match_term