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

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