Introduction

Rewriting  is basically the process of using equations as transformational rules.

In Nuprl, rewrite rules  are derived from

• abstractions,
• primitive reduction rules, and
• formulas of form

  

  that occur as lemmas or hypotheses.

Nuprl's rewrite package is a collection of ML functions for creating rewrite rules and applying them in various fashions to clauses of a sequent.

The package supports rewrite rules involving various equivalence relations. Examples include the 3-place equality-in-a-type  relation, the iff relation  , and the permutation relation  on lists. Nuprl's logic doesn't guarantee that all equivalence relations are respected. In cases when there is no guarantee, the package takes care of automating proofs that the relations are respected.

The notion of rewriting is extended to including rules involving any transitive relation. Here, the package takes care of checking that relevant terms are appropriately monotonic.

The package is based around ML objects of type convn called conversions , similar to those found in other tactic based theorem provers such as LCF  , HOL  and Isabelle  . Conversions provide a language for systematically building up rewrite rules in a fashion similar to the way tactics are assembled using tacticals.

For convenience, a few concise rewriting tactics are provided that completely hide the conversion language (see Section ). These are sufficient in many situations, though most Nuprl users will need eventually to familiarize themselves with many of the details of the package.

Note that Section describes some older substitution tactics that can be used for certain very simple kinds of rewriting.