FIRST_ASSUM : thm_tactic -> tactic
Applied theorem-tactic to first assumption possible.
has the effect of applying the first tactic which can be produced by
ttac from the assumptions (.. |- A1), ..., (.. |- An) and which
succeeds when applied to the goal. Failures of ttac to produce a tactic are
ignored. The similar function FIRST_X_ASSUM is the same except that the
assumption used is then removed from the goal.
FIRST_ASSUM ttac ([A1; ...; An], g)
- FAILURE CONDITIONS
Fails if ttac (.. |- 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.
searches the assumptions for either a contradiction or the desired
conclusion. The tactic
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 (fun asm -> CONTR_TAC asm ORELSE ACCEPT_TAC asm)
- SEE ALSO
ASSUM_LIST, EVERY, EVERY_ASSUM, FIRST, FIRST_X_ASSUM, MAP_EVERY, MAP_FIRST.