RESQ_RES_THEN

res_quanLib.RESQ_RES_THEN : thm_tactic -> tactic

Resolves all restricted universally quantified assumptions against other assumptions of a goal.

Like the function RESQ_IMP_RES_THEN, the function RESQ_RES_THEN performs a single step resolution. The difference is that the restricted universal quantification used in the resolution is taken from the assumptions.

Given a theorem-tactic ttac, applying the tactic RESQ_RES_THEN ttac to a goal (asml,gl) has the effect of:

   MAP_EVERY (mapfilter ttac [... ; (ai,aj |- vi) ; ...]) (amsl ?- g)

where the theorems ai,aj |- vi are all the consequences that can be drawn by a (single) matching modus-ponens inference from the assumptions amsl and the implications derived from the restricted universal quantifications in the assumptions.

Failure

Evaluating RESQ_RES_TAC ttac th fails if there are no restricted universal quantifications in the assumptions, or if the theorem-tactic ttac applied to all the consequences fails.

See also

res_quanLib.RESQ_IMP_RES_TAC, res_quanLib.RESQ_IMP_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