# A Formalised First-Order Confluence Proof for the Lambda-Calculus using
One-Sorted Variable Names

## (Barendregt was right after all ... almost)

### Authors: Rene Vestergaard and James Brotherston

The Isabelle theories below comprise the entire Isabelle
/ HOL implementation of the titular proof development as given in
the article. All proofs are due to the authors, with the
exception of the proofs in the Commutation theory, for which we thank
Tobias Nipkow. Queries
or comments are naturally welcome and may be directed either to Rene Vestergaard or James Brotherston.

View theory dependencies

## Isabelle / HOL Theories

### High-level:

- RawToReal -
Confluence of the real lambda-calculus
- AbstractRewrites -
Preservation / reflection of diamond property across structural collapse
- RawConfluence -
Confluence of the raw lambda-calculus
- AlphaBetaDiamond -
Diamond property of the "middle relation" (->>A; -|>B)

### Mid-level:

- Commutation -
Abstract commutation and confluence notions, including Tait/Martin-Lof theorem
- DiamondPB -
Diamond property of parallel beta via complete developments (Takahashi's Trick)
- ExistsBCF -
Existence of (fresh-naming) alpha-rewrite sequence from any term to a BCF term
- FreshAlphaConf -
Confluence property of the fresh-naming alpha relation, ->A0
- ParBeta -
Substitutivity and other properties of the parallel beta relation, -|>B
- WeakABComm -
Weak commutativity of fresh-naming alpha and parallel beta

### Low-level:

- Alpha -
Definition and properties - in particular, symmetry - of the alpha relation
- AlphaZero -
Definition and properties of various formulations of the fresh-naming
alpha relation
- AlphaClass -
Definition and basic properties of the function returning the
alpha-equivalence class of a term
- Beta -
Definition of the standard raw beta relation, ->B
- Lambda -
Definition of terms and substitution in the raw calculus, plus renaming lemmas
- SubstLemmas -
Substitution lemmas on the raw calculus
- VarList -
Properties of lists of one-sorted variable names
- Variables -
Properties of the set of one-sorted variable names - in particular, the guaranteed existence of fresh names