Constructive Rewriting

Tobias Nipkow

The subject of this paper is rewriting in an LCF-like general theorem proving framework. It is shown how rewriting of both terms and formulae can be implemented by simple tactics in the generic theorem prover Isabelle. These tactics can easily be combined with induction to yield powerful theorem proving primitives. As a sample application the verification of an n-bit ripple-carry adder is demonstrated.


@article{Nipkow-CJ-91, author="Tobias Nipkow", title="Constructive Rewriting", journal="Computer Journal",year=1991,volume=34,pages="34--41"}