CONSEQ_TOP_REWRITE_CONV

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

An extended version of MATCH_MP.

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.

See also

Drule.MATCH_MP, ConseqConv.CONSEQ_REWRITE_CONV, ConseqConv.DEPTH_CONSEQ_CONV