PAT_ASSUM

Tactical.PAT_ASSUM : term -> thm_tactic -> tactic

Finds the first assumption that matches the term argument, applies the theorem tactic to it. The matching assumption remains in the assumption list.

The tactic

   PAT_ASSUM tm ttac ([A1, ..., An], g)

finds the first Ai which matches tm using higher-order pattern matching in the sense of ho_match_term. Free variables in the pattern that are also free in the assumptions or the goal must not be bound by the match. In effect, these variables are being treated as local constants.

Failure

Fails if the term doesn’t match any of the assumptions, or if the theorem-tactic fails when applied to the first assumption that does match the term.

Example

The tactic

   PAT_ASSUM ``x:num = y`` SUBST_ALL_TAC

searches the assumptions for an equality over numbers and causes its right hand side to be substituted for its left hand side throughout the goal and assumptions. It also removes the equality from the assumption list. Trying to use FIRST_ASSUM above (i.e., replacing PAT_ASSUM with FIRST_ASSUM and dropping the term argument entirely) would require that the desired equality was the first such on the list of assumptions.

If one is trying to solve the goal

   { !x. f x = g (x + 1), !x. g x = f0 (f x)} ?- f x = g y

rewriting with the assumptions directly will cause a loop. Instead, one might want to rewrite with the formula for f. This can be done in an assumption-order-independent way with

   PAT_ASSUM (Term`!x. f x = f' x`) (fn th => REWRITE_TAC [th])

This use of the tactic exploits higher order matching to match the RHS of the assumption, and the fact that f is effectively a local constant in the goal to find the correct assumption.

Comments

The behavior of PAT_ASSUM changed in Kananaskis 12. The old PAT_ASSUM (and qpat_assum, Q.PAT_ASSUM) was changed to include an extra _X_ (or _x_), indicating that the matching assumption is pulled out of the assumption list. The old name now provides a version that doesn’t pull the assumption out of the list.

See also

Tactical.PAT_X_ASSUM, Tactical.ASSUM_LIST, Tactical.EVERY, Tactical.EVERY_ASSUM, Tactical.FIRST, Tactical.MAP_EVERY, Tactical.MAP_FIRST, Thm_cont.UNDISCH_THEN, Term.match_term