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.
BibTeX:
<![CDATA[
@article{Nipkow-CJ-91,
author="Tobias Nipkow",
title="Constructive Rewriting",
journal="Computer Journal",year=1991,volume=34,pages="34--41"}
]]></plaintext></p></div></div>