Constructive Rewriting
Tobias Nipkow · The Computer Journal · 1991
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.