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