Tactic.MATCH_MP

STRUCTURE

SYNOPSIS

Reduces the goal using a supplied implication, with matching.

DESCRIPTION

When applied to a theorem of the form

   A' |- !x1...xn. s ==> !y1...ym. t

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 ?- !v1...vi. t'
  ======================  MATCH_MP_TAC (A' |- !x1...xn. s ==> !y1...ym. t)
     A ?- ?z1...zp. s'

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.

FAILURE

Fails unless the theorem is an (optionally universally quantified) implication whose consequent can be instantiated to match the goal. The generalized variables v1, ..., vi must occur in s' in order for the conclusion t of the supplied theorem to match t'.

COMMENTS

The tactic irule builds on MATCH_MP_TAC, normalising the input theorem more aggressively so that it succeeds more often.

SEEALSO

CONSEQ_CONV_TAC, EQ_MP, irule, MATCH_MP, MP, MP_TAC