MATCH_MP_TAC : thm_tactic
Reduces the goal using a supplied implication, with matching.
When applied to a theorem of the form
MATCH_MP_TAC produces a tactic that reduces a goal whose conclusion
t' is a substitution and/or type instance of t to the corresponding
instance of s. Any variables free in s but not in t will be existentially
quantified in the resulting subgoal:
where z1, ..., zp are (type instances of) those variables among
x1, ..., xn that do not occur free in t. Note that this is not a valid
tactic unless A' is a subset of A.
A ?- t'
====================== MATCH_MP_TAC (A' |- !x1...xn. s ==> t)
A ?- ?z1...zp. s'
The following goal might be solved by case analysis:
We can ``manually'' perform induction by using the following theorem:
# g `!n:num. n <= n * n`;;
which is useful with MATCH_MP_TAC because of higher-order matching:
val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)
The goal can be finished with ARITH_TAC.
# e(MATCH_MP_TAC num_INDUCTION);;
val it : goalstack = 1 subgoal (1 total)
`0 <= 0 * 0 /\ (!n. n <= n * n ==> SUC n <= SUC n * SUC n)`
- FAILURE CONDITIONS
Fails unless the theorem is an (optionally universally quantified) implication
whose consequent can be instantiated to match the goal.
- SEE ALSO
EQ_MP, MATCH_MP, MP, MP_TAC, PART_MATCH.