conseq_conv

ConseqConv.type conseq_conv

A type for functions that given a term produce a theorem with an implication at the top level.

Classical conversions (see Conv) convert a given term t to a term eqt that is equal to t. For a boolean term t, it is however sometimes useful not to preserve equivalence, but to either strengthen t to st or to weaken it to wt. The type conseq_conv is used for ML functions that perform these operations. These ML Functions are called consequence conversions in the following.

Given a consequence conversion CONSEQ_CONV and a term t, then CONSEQ_CONV can either fail with an HOL_ERR-exception, raise an UNCHANGED-exception or produce a theorem of one of the following forms:

   1. st ==> t
   2. t ==> wt
   3. t = eqt

Example

Examples of simple consequence conversion are TRUE_CONSEQ_CONV and FALSE_CONSEQ_CONV.

See also

ConseqConv.directed_conseq_conv, ConseqConv.TRUE_FALSE_REFL_CONSEQ_CONV