RESQ_IMP_RES_THEN
res_quanLib.RESQ_IMP_RES_THEN : thm_tactical
Resolves a restricted universally quantified theorem with the assumptions of a goal.
The function RESQ_IMP_RES_THEN is the basic building block for
resolution using a restricted quantified theorem. It takes a restricted
quantified theorem and transforms it into an implication. This resulting
theorem is used in the resolution.
Given a theorem-tactic ttac and a theorem th, the theorem-tactical
RESQ_IMP_RES_THEN transforms the theorem into an implication th'. It
then passes th' together with ttac to IMP_RES_THEN to carry out
the resolution.
Failure
Evaluating RESQ_IMP_RES_THEN ttac th fails if the supplied theorem
th is not restricted universally quantified, or if the call to
IMP_RES_THEN fails.
See also
res_quanLib.RESQ_IMP_RES_TAC,
res_quanLib.RESQ_RES_THEN,
res_quanLib.RESQ_RES_TAC,
Thm_cont.IMP_RES_THEN,
Tactic.IMP_RES_TAC,
Drule.MATCH_MP,
Drule.RES_CANON,
Tactic.RES_TAC,
Thm_cont.RES_THEN