Abstract: Theorem Reuse by Proof Term Transformation

Theorem Reuse by Proof Term Transformation

Einar Broch Johnsen
Department of Informatics, University of Oslo

Christoph Lüth
FB 3 - Mathematik und Informatik, Universität Bremen

Proof reuse addresses the issue of how proofs of theorems in a
specific setting can be used to prove other theorems in different
settings. This paper proposes an approach where theorems are
generalised by abstracting their proofs from the original
setting. The approach is based on a representation of proofs as
logical framework proof terms, using the theorem prover Isabelle.
The logical framework allows type-specific inference rules to be
handled uniformly in the abstraction process and the prover's
automated proof tactics may be used freely. This way, established
results become more generally applicable; for example, theorems
about a data type can be reapplied to other types. The paper also
considers how to reapply such abstracted theorems, and suggests an
approach based on mappings between operations and types, and on
systematically exploiting the dependencies between theorems.