Generates a tactic from the assumptions, discards the assumptions and
applies the tactic.
DESCRIPTION
When applied to a function and a goal, POP_ASSUM_LIST applies
the function to a list of theorems corresponding to the
assumptions of the goal, then applies the resulting tactic to the goal
with an empty assumption list.
POP_ASSUM_LIST f ({A1;...;An} ?- t) = f [.. |- A1; ... ; .. |- An] (?- t)
FAILURE CONDITIONS
Fails if the function fails when applied to the list of assumptions, or if the
resulting tactic fails when applied to the goal with no assumptions.
COMMENTS
There is nothing magical about POP_ASSUM_LIST: the same effect can be
achieved by using ASSUME a explicitly wherever the assumption a is
used. If POP_ASSUM_LIST is used, it is unwise to select elements by
number from the ASSUMEd-assumption list, since this introduces a dependency
on ordering.
EXAMPLE
We can collect all the assumptions of a goal into a conjunction and make them a
new antecedent by:
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ)
USES
Making more delicate use of the assumption list than simply rewriting etc.