HO_MATCH_MP_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Reduces the goal using a supplied implication, with higher-order matching.
- DESCRIPTION
- When applied to a theorem of the formHO_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:
A' |- !x1...xn. s ==> t

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' ====================== HO_MATCH_MP_TAC (A' |- !x1...xn. s ==> t) A ?- ?z1...zp. s'

- EXAMPLE
- 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 HO_MATCH_MP_TAC because of higher-order matching:> numTheory.INDUCTION; - val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)

The goal can be finished with SIMP_TAC arith_ss [].> e(HO_MATCH_MP_TAC numTheory.INDUCTION); - val it : goalstack = 1 subgoal (1 total) `0 <= 0 * 0 /\ (!n. n <= n * n ==> SUC n <= SUC n * SUC n)`

- FAILURE
- Fails unless the theorem is an (optionally universally quantified) implication whose consequent can be instantiated to match the goal.
- SEEALSO

HOL Kananaskis-14