Tactical.PAT

STRUCTURE

SYNOPSIS

Finds the first assumption that matches the term argument, applies the theorem tactic to it, and removes this assumption.

DESCRIPTION

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. Unless there is just one match otherwise, 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 (Term`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, and would leave an equality on the assumption list of the form x = x.

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.

SEEALSO

ASSUM_LIST, EVERY, EVERY_ASSUM, FIRST, MAP_EVERY, MAP_FIRST, UNDISCH_THEN, match_term