CHECK_ASSUME_TAC
Tactic.CHECK_ASSUME_TAC : thm_tactic
Adds a theorem to the assumption list of goal, unless it solves the goal.
When applied to a theorem A' |- s and a goal A ?- t, the tactic
CHECK_ASSUME_TAC checks whether the theorem will solve the goal (this
includes the possibility that the theorem is just A' |- F). If so, the
goal is duly solved. If not, the theorem is added to the assumptions of
the goal, unless it is already there.
A ?- t
============== CHECK_ASSUME_TAC (A' |- F) [special case 1]
A ?- t
============== CHECK_ASSUME_TAC (A' |- t) [special case 2]
A ?- t
============== CHECK_ASSUME_TAC (A' |- s) [general case]
A u {s} ?- t
Unless A' is a subset of A, the tactic will be invalid, although it
will not fail.
Failure
Never fails.
See also
Tactic.ACCEPT_TAC,
Tactic.ASSUME_TAC,
Tactic.CONTR_TAC,
Tactic.DISCARD_TAC,
Tactic.MATCH_ACCEPT_TAC