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 general-purpose "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, user-defined 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 built-in 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 domain-specific tactics.

  This project aims to give end-users 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 user-maintainable medium for storing a common piece of reasoning between proofs that has been identified post-hoc.

• 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

		Daniel Matichuk Automation for proof engineering: Machine-checked proofs at scale PhD Thesis, UNSW, Sydney, Australia, 2018
		Daniel Matichuk, Toby Murray and Makarius Wenzel Eisbach: A proof method language for isabelle Journal of Automated Reasoning, Volume 56, Number 3, pp. 261–282, March, 2016
		Daniel Matichuk, Makarius Wenzel and Toby Murray An Isabelle proof method language International Conference on Interactive Theorem Proving, pp. 390–405, Vienna, Austria, July, 2014

People