The Mechanisation of Barendregt-Style Equational Proofs
(The Residual Perspective)
Authors: Rene Vestergaard and James Brotherston
The Isabelle theories below comprise the Isabelle
/ HOL implementation of the proof of the results in section 3 of the
the article. All proofs are due to the authors. Queries
or comments are naturally welcome and may be directed either to Rene Vestergaard or James Brotherston.
View theory dependencies
Theories
- Variables - Definition and properties
of the set of one-sorted variable names - in particular, the
guaranteed existence of fresh names
- MarkedLambda - Definition of
(marked) terms and substitution in the raw calculus, plus renaming and
substitution lemmas
- ResidualBeta - Proof of non-blocked
BCF-initial beta-residual theory , plus auxiliary lemmas