PRED_ASSUM

Tactical.PRED_ASSUM : (term -> bool) -> thm_tactic -> tactic

Discharges a selected assumption and passes it to a theorem-tactic.

PRED_ASSUM finds the first assumption satisfying the prediate given, removes it from the assumption list, ASSUMEs it, passes it to the theorem-tactic and then applies the consequent tactic. Thus, where t is the first assumption satisfying p,

   PRED_ASSUM p f ([a1,... ai, t, aj, ... an], goal) =
     f (ASSUME t) ([a1,... ai, aj,... an], goal)

For example (again, where t is the first assumption in A u {t} satisfying p), if

    A ?- c
   ========  f (ASSUME t)
    B ?- v

then

    A u {t} ?- c
   ===============  PRED_ASSUM p f
       B ?- v

Failure

PRED_ASSUM p will fail on goals where no assumption safisfies p.

See also

Thm_cont.UNDISCH_THEN, Tactical.PAT_ASSUM, Tactical.POP_ASSUM, Tactic.UNDISCH_TAC