----------------------------------------------------------------------
CONSEQ_TOP_REWRITE_CONV                                   (ConseqConv)
----------------------------------------------------------------------
CONSEQ_TOP_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv

SYNOPSIS
An extended version of {MATCH_MP}.

DESCRIBE
This consequence conversion gets 3 lists of theorems as parameters:
{both_thmL}, {strengthen_thmL} and {weaken_thmL}.
The theorems in these lists are used to strengthen or weaken a given
boolean term at toplevel. If using them for strengthening this consequence
conversion behaves similar to MATCH_MP. As the names suggest, the
theorems in {strengthen_thmL} are used for strengthening, the ones in
{weaken_thmL} for weakening and the ones in {both_thmL} for both.

Before trying to apply the conversion, the theorem lists are
preprocessed.  The theorems are split along conjunctions and
allquantification is removed. Then theorems with toplevel negation
{|- ~P} are rewritten to {|- P = F}. Afterwards every theorem {|- P} that
is not an implication or an boolean equation is replaced by
{|- P = T}. Finally, boolean equations {|- P = Q} are splitted into two
theorems {|- P ==> Q} and {|- Q ==> P}. One ends up with a list of
implications.

Given a term {t} the conversion tries
to find a theorem {|- P ==> Q} and - depending on to the direction -
strengthen {t} by matching it with {Q} or weaken it by
matching it with {P}.

EXAMPLE
This directed consequence conversion is intended to be used together
with {DEPTH_CONSEQ_CONV}. The combination of both is called
{CONSEQ_REWRITE_CONV}. Please have a look there for an example.



SEEALSO
Drule.MATCH_MP, ConseqConv.CONSEQ_REWRITE_CONV,
ConseqConv.DEPTH_CONSEQ_CONV.

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