More Church–Rosser Proofs

The proofs of the Church–Rosser theorems for β, η, and β ∪ η reduction in untyped λ-calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For β-reduction, both the standard proof and Takahashi's are given and compared. All proofs are based on a general theory of commutating relations that supports an almost geometric style of reasoning about confluence diagrams.