LP, the Larch Prover — The normalize command

The normalize command provides manual control over the application of (possibly passive) rewrite rules to (possibly immune) formulas, rewrite rules, and deduction rules. It also provides a means of backward inference.

Syntax

<normalize-command> ::= normalize <target> [ with [ reversed ] <names> ]
<target>            ::= <names> | conjecture

Examples

normalize immune / lemmas with *
normalize conjecture with distributiveLaws

Usage

The first version of the normalize command normalizes the formulas, deduction rules, and rewrite rules in the <target>, whether or not they are immune, using the hardwired rewrite rules together with the rewrite rules obtained as described below. Rewrite rules in the <target> that are also named by <names> are not normalized.

If reversed is present, all named formulas and rewrite rules, whether or not they are active, that can be oriented from right to left into legal rewrite rules are used with that orientation. If reversed is not present, all named rewrite rules and formulas, whether or not they are active, that can be oriented from left to right are used with that orientation. If no <names> are given, all rewrite rules and left-to-right orientable formulas are used.

The second version of the normalize command normalizes the current conjecture using the rewrite rules obtained as just described.

The normalize command is typically used to ``open up'' definitions using a set of passive rewrite rules. When reversed is present, the named rewrite rules should ordinarily be passive to prevent them from immediately undoing the result of the normalize command. See also the rewrite command.