Rewrite.FILTER_ASM_REWRITE

STRUCTURE

SYNOPSIS

Rewrites a theorem including built-in rewrites and some of the theorem’s assumptions.

DESCRIPTION

This function implements selective rewriting with a subset of the assumptions of the theorem. The first argument (a predicate on terms) is applied to all assumptions, and the ones which return true are used (along with the set of basic tautologies and the given theorem list) to rewrite the theorem. See GEN_REWRITE_RULE for more information on rewriting.

FAILURE

FILTER_ASM_REWRITE_RULE does not fail. Using FILTER_ASM_REWRITE_RULE may result in a diverging sequence of rewrites. In such cases FILTER_ONCE_ASM_REWRITE_RULE may be used.

USES

This rule can be applied when rewriting with all assumptions results in divergence. Typically, the predicate can model checks as to whether a certain variable appears on the left-hand side of an equational assumption, or whether the assumption is in disjunctive form.

Another use is to improve performance when there are many assumptions which are not applicable. Rewriting, though a powerful method of proving theorems in HOL, can result in a reduced performance due to the pattern matching and the number of primitive inferences involved.

SEEALSO

ASM_REWRITE_RULE, FILTER_ONCE_ASM_REWRITE_RULE, FILTER_PURE_ASM_REWRITE_RULE, FILTER_PURE_ONCE_ASM_REWRITE_RULE, GEN_REWRITE_RULE, ONCE_REWRITE_RULE, PURE_REWRITE_RULE, REWRITE_RULE