POP_LAST_ASSUM

Tactical.POP_LAST_ASSUM : thm_tactic -> tactic

Applies tactic generated from the last element of a goal’s assumption list.

When applied to a theorem-tactic and a goal, POP_LAST_ASSUM applies the theorem-tactic to the ASSUMEd last element of the assumption list, and applies the resulting tactic to the goal without that assumption in its assumption list:

   POP_LAST_ASSUM f ({A1,...,Am,An} ?- t) = f (An |- An) ({A1,...,Am} ?- t)

Failure

Fails if the assumption list of the goal is empty, or the theorem-tactic fails when applied to the popped assumption, or if the resulting tactic fails when applied to the goal (with depleted assumption list).

Comments

The tactical POP_LAST_ASSUM is also available under the lower-case version of the name, pop_last_assum.

See also

Tactical.ASSUM_LIST, Tactical.EVERY_ASSUM, Tactic.IMP_RES_TAC, Tactical.POP_ASSUM, Rewrite.REWRITE_TAC