FIRST_ASSUM : (thm_tactic -> tactic)

- STRUCTURE
- SYNOPSIS
- Maps a theorem-tactic over the assumptions, applying first successful tactic.
- DESCRIPTION
- The tactichas the effect of applying the first tactic which can be produced by ttac from the ASSUMEd assumptions (A1 |- A1), ..., (An |- An) and which succeeds when applied to the goal. Failures of ttac to produce a tactic are ignored.
FIRST_ASSUM ttac ([A1; ...; An], g)

- FAILURE
- Fails if ttac (Ai |- Ai) fails for every assumption Ai, or if the assumption list is empty, or if all the tactics produced by ttac fail when applied to the goal.
- EXAMPLE
- The tacticsearches the assumptions for either a contradiction or the desired conclusion. The tactic
FIRST_ASSUM (fn asm => CONTR_TAC asm ORELSE ACCEPT_TAC asm)

searches the assumption list for an implication whose conclusion matches the goal, reducing the goal to the antecedent of the corresponding instance of this implication.FIRST_ASSUM MATCH_MP_TAC

- COMMENTS
- By default, the assumption list is printed in reverse order, with the head of the list printed last. To process the assumption list in the opposite order, use LAST_ASSUM
- SEEALSO

HOL Kananaskis-13