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