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

SYNOPSIS

Applies a tactic generated from the goal's assumption list.

DESCRIPTION

When applied to a function of type thm list -> tactic and a goal, ASSUM_LIST constructs a tactic by applying f to a list of ASSUMEd assumptions of the goal, then applies that tactic to the goal.

   ASSUM_LIST f ({A1;...;An} ?- t)
         = f [A1 |- A1; ... ; An |- An] ({A1;...;An} ?- t)

FAILURE CONDITIONS

Fails if the function fails when applied to the list of ASSUMEd assumptions, or if the resulting tactic fails when applied to the goal.

COMMENTS

There is nothing magical about ASSUM_LIST: the same effect can usually be achieved just as conveniently by using ASSUME a wherever the assumption a is needed. If ASSUM_LIST is used, it is extremely unwise to use a function which selects elements from its argument list by number, since the ordering of assumptions should not be relied on.

EXAMPLE

The tactic:

   ASSUM_LIST(MP_TAC o end_itlist CONJ)

adds a conjunction of all assumptions as an antecedent of a goal.

USES

Making more careful use of the assumption list than simply rewriting.