Eisbach: High Level Proof Methods for Isabelle
The Eisbach project has successfully concluded with Daniel Matichuk's PhD thesis (see below in publications). The Eisbach proof method language is now available in the Isabelle distribution.
Below is an archive of the original project goals and web page.
Aim: Enable users to easily write automated reasoning procedures (proof methods) in Isabelle.
Overview: To facilitate larger and more ambitious proofs there has been much research into automated reasoning techniques for interactive theorem provers. These often come in the form of generalpurpose "tactics" which solve a particular class of problem or simplify proof states to make further reasoning more straightforward. Tactics are generally written in the implementation language of the theorem prover, making them difficult to implement or extend by the typical end user.
In Coq, userdefined tactics can be written in the language "Ltac". While not exposing the generality of the underlying ocaml implementation, it has proven to be sufficient for a large amount of automation. The builtin automated tactics in Coq, however, are relatively weak compared to those of Isabelle, essentially requiring that any significant proof development have its own collection of domainspecific tactics.
This project aims to give endusers the ability to define automated proof techniques for Isabelle at a high level of abstraction, circumventing the overhead of learning the underlying ML API. Similar to Ltac, the goal is to create a language in which users can define tactics at a similar level of abstraction to proof scripts. However, by leveraging the existing powerful automated tactics within Isabelle, the language will have a focus on high level proof strategies. Specifically it will be designed to be a usermaintainable medium for storing a common piece of reasoning between proofs that has been identified posthoc.

Technical research challenges:
 Investigate useful features for a method language in Isabelle and determine the appropriate level of abstraction.
 Develop Eisbach as an extension to Isabelle, integrating with existing automated proof methods and Isabelle syntax.
Publications
People
Past
