POP_ASSUM_LIST : (thm list -> tactic) -> tactic

- STRUCTURE
- SYNOPSIS
- 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 ASSUMEd 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 |- A1, ..., An |- An] (?- t)

- FAILURE
- Fails if the function fails when applied to the list of ASSUMEd 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
- Suppose we have a goal of the following form:Then we can split the conjunctions in the assumption list apart by applying the tactic:
{a /\ b, c, (d /\ e) /\ f} ?- t

which results in the new goal:POP_ASSUM_LIST (MAP_EVERY STRIP_ASSUME_TAC)

{a, b, c, d, e, f} ?- t

- USES
- Making more delicate use of the assumption list than simply rewriting or using resolution.
- SEEALSO

HOL Kananaskis-13