Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof

We discuss methods for dealing effectively with let-bindings in proofs. Our contribution is a small set of unconditional rewrite rules, found by the bracket abstraction translation from the λ-calculus to combinators. This approach copes with the usual HOL encodings of paired ion, ensures that bound variable names are preserved, and uses only conventional simplification technology.

• Type: Conference
• Year: 2005
• Where: TPHOL
• Authors: Michael Norrish, Konrad Slind
• Keywords: Artificial Intelligence, Bracket Abstraction Translation, TPHOL 2005, Unconditional Rewrite Rules, Usual Hol Encodings