ConseqConv.CONSEQ_REWRITE

STRUCTURE

SYNOPSIS

Applies CONSEQ_TOP_REWRITE_CONV repeatedly at subterms.

DESCRIPTION

This directed consequence conversion is a combination of CONSEQ_TOP_REWRITE_CONV and DEPTH_CONSEQ_CONV. Given lists of theorems, these theorems are preprocessed to extract implications. Then these implications are used to either weaken or strengthen an input term.

EXAMPLE

Reconsider the example for DEPTH_CONSEQ_CONV. Let rewrite_every_thm be the following theorem:

   val rewrite_every_thm =
       |- FEVERY P FEMPTY /\
          (FEVERY P f /\ P (x,y) ==> FEVERY P (f |+ (x,y)));

Then the following call of CONSEQ_REWRITE_CONV

   CONSEQ_REWRITE_CONV ([], [rewrite_every_thm], []) CONSEQ_CONV_STRENGTHEN_direction
     ``!y2. FEVERY P (f |+ (x1, y1) |+ (x2,y2)) /\ Q z``

results in

    |- (!y2. ((FEVERY P f /\ P (x1, y1)) /\ P (x2,y2)) /\ Q z) ==>
       (!y2. FEVERY P (f |+ (x1, y1) |+ (x2,y2)) /\ Q z)

More examples can be found at the end of ConseqConv.sml.

SEEALSO

MATCH_MP, CONSEQ_TOP_REWRITE_CONV, DEPTH_CONSEQ_CONV, EXT_CONSEQ_REWRITE_CONV