The Mechanisation of
          Barendregt-Style Equational Proofs
              (the Residual Perspective)

        Rene Vestergaard and James Brotherston


We show how to mechanise equational proofs about higher-order
languages by using the primitive proof principles of first-order
abstract syntax over one-sorted variable names. We illustrate the
method here by proving (in Isabelle/HOL) a technical property
which makes the method widely applicable for the lambda-calculus:
the residual theory of beta is renaming-free up-to an initiality
condition akin to the so-called Barendregt Variable Convention. We
use our results to give a new diagram-based proof of the
development part of the strong finite development property for the
lambda-calculus. The proof has the same equational implications
(e.g., confluence) as the proof of the full property but without
the need to prove SN. We account for two other uses of the proof
method, as presented elsewhere. One has been mechanised in full in
Isabelle/HOL.