----------------------------------------------------------------------
RESQ_REWRITE1_TAC                                        (res_quanLib)
----------------------------------------------------------------------
RESQ_REWRITE1_TAC : thm_tactic

SYNOPSIS
Rewriting with a restricted universally quantified theorem.

KEYWORDS
tactic, rewriting, restricted quantifier.

DESCRIBE
{RESQ_REWRITE1_TAC} takes an equational theorem which is restricted universally
quantified at the outer level. It calls {RESQ_REWR_CANON} to convert
the theorem to the form accepted by {COND_REWR_TAC} and passes the
resulting theorem to this tactic which carries out conditional
rewriting.

Suppose that {th} is the following theorem

   A |- !x::P. Q[x] = R[x])

Applying the tactic {RESQ_REWRITE1_TAC th} to a goal {(asml,gl)}
will return a main subgoal {(asml',gl')} where {gl'} is obtained by
substituting instances of {R[x'/x]} for corresponding instances of
{Q[x'/x]} in the original goal {gl}. All instances of {P x'} which
do not appear in the original assumption {asml} are added to it to
form {asml'}, and they also become new subgoals {(asml,P x')}.

FAILURE
{RESQ_REWRITE1_TAC th}  fails if {th} cannot be transformed into the
required form by the function {RESQ_REWR_CANON}. Otherwise, it fails if no
match is found or the theorem cannot be instantiated.



SEEALSO
res_quanLib.RESQ_REWRITE1_CONV, res_quanLib.RESQ_REWR_CONV.

----------------------------------------------------------------------