Eisbach: A Proof Method Language for Isabelle

摘要

Machine-checked proofs are becoming ever-larger, presenting an increasing maintenance challenge. Isabelle's most popular language interface, Isar, is attractive for new users, and powerful in the hands of experts, but has previously lacked a means to write automated proof procedures. This can lead to undesirable duplication in large proofs. In this paper we present Eisbach, a proof method language for Isabelle, which aims to fill this gap by incorporating Isar language elements, thus making it accessible to end-users. We describe the language and the design principles on which it was developed. We evaluate its effectiveness by implementing the most-widely used proof tools in the seL4 verification stack, and consider its strengths and limitations.