Eisbach : High Level Proof Methods for Isabelle
Eisbach is a research activity of the Trustworthy Systems Group.
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.
|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