ConseqConv.CONSEQ_TOP_REWRITE

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.