Isabelle for Rodin

This plug-in provides an automated proof tactic based on the theorem prover Isabelle/HOL. It also allows users to export proof obligations to Isabelle theories for later inspection with Isabelle. Some of the theoretical foundations are described in . More information will become available in .

Installation

The installation consists of the following steps:

1. Install the Rodin feature Isabelle for Rodin.
2. Install Isabelle.
3. Install the Isabelle logic HOL-EventB.
4. Connect Isabelle to Rodin.

Rodin Feature

The feature can be installed using Rodin's software installation facilities and is available on Rodin's main update site (http://rodin-b-sharp.sourceforge.net/updates at time of writing) in the category Prover Extensions.

Please make sure that

• the Scala update site http://download.scala-ide.org/releases/2.0.0-beta appears in the list of available software sites, and
• the box "contact all update sites during install to find required software" is checked.

Isabelle

Installation instructions for Isabelle can be found here. The main executable is ${ISABELLE_HOME}/bin/isabelle, where ${ISABELLE_HOME} is the root directory of the Isabelle installation. It may be useful to install this executable somewhere on the search path of your operating system; use "isabelle install" to do so.

HOL-EventB

Download the HOL-EventB*.tgz archive from http://sourceforge.net/projects/rodin-b-sharp/files/Plugin_Isabelle/. The version of HOL-EventB has to coincide with the version of the Isabelle for Rodin feature! Extract it to a location of your choice. Change to the newly generated directory and invoke "isabelle make". This makes the HOL-EventB logic available to Isabelle.

Connect Isabelle to Rodin

Back to Rodin, go to the Preferences dialog. Navigate to the "Isabelle for Rodin" section. Make sure that the "Isabelle executable" is correctly chosen. You may enter an absolute path or a path relative to the search path or a path relative to your current work directory. Press the "Test" button to test your Isabelle installation.

Limitation on Windows: so far, it is impossible to launch Isabelle from Rodin under Windows. More precisely, it may be possible, but it is unclear how to set the preferences.

Usage

Proving Proof Obligations

To make Isabelle available as auto-tactic you have to define a parameterized tactic as follows. Search for the Auto/Post Tactic section in the Preferences dialog. Generate a new profile. As "kind" of the profile choose "Parameterized Tactic". Choose Isabelle as the tactic to be parameterized.

Back to the Auto/Post Tactic section choose the newly generated Isabelle profile as the profile used by the auto-tactic. Alternatively, you may include the Isabelle profile in another profile of the kind "Combined Tactic".

The Isabelle feature also supplies several buttons in the proof control view.

Exporting Proof Obligations

You may export the proof obligations associated with a project or component (e.g. context or machine) as follows:

• Right-click some proof obligation(s) in the project explorer.
• Choose "Export to Isabelle".

The plug-in will create "isabelle" subfolders in every involved project folder and put the translations of the proof obligations into these folders. For every component (context or machine) two theory files will be generated: one storing the selected proof obligations of that component and the other one containing proof attempts.

The Isabelle feature also supplies a button in the proof control view to export the sequent of the current proof attempt.

Limitations

Version 0.6.0 has a number of limitations. Solutions to these problems are available, but they still need to be implemented.

• Support for Windows is limited. Export of proof obligations does work. Invoking Isabelle from Rodin does not. The problem is to launch Isabelle through Cygwin from a DOS shell.
• The Isabelle plug-in is slower than it could be for two reasons:
  • Isabelle is restarted for each proof attempt. Starting Isabelle (without starting a proof attempt) takes several seconds.
  • Isabelle's generic parser is used to parse the theories generated by Rodin.
• The names of variables may clash with reserved keywords in Isabelle/EventB. The plug-in maintains a possibly incomplete blacklist of reserved keywords. A name clash may only occur with keywords that do not occur on this blacklist. In practice, such a name clash is therefore rather unlikely (i.e., it has never been observed). The most likely consequence of a name clash is a parse error.
• The names of theories that result from exporting proof obligations may clash with the names of built-in theories of HOL or HOL-EventB. The consequence is that the generated theory cannot be loaded in Isabelle.

News

Version 0.6.0

Rodin Plug-ins:

• integrated Isabelle as a reasoner / tactic
• tested the Isabelle integration on Linux and MaxOS; the integration does not yet work on Windows
• preference dialogs for configuring Isabelle
• various simplifications of the user interaction

HOL-EventB:

• upgrade to Isabelle2011-1
• fixed a problem with printing of sequents
• a command assert_finished that checks whether a proof is finished and emits an error otherwise
• sensible default configuration for axe'
• make use of smt_certificates so that users without Z3 can build EventB

Version 0.5.0

Rodin Plug-ins:

• (incompatible) changes in translation, taking changes in HOL/Event-B into account
• infrastructure for doing the experiments of my PhD thesis
• a plug-in for generating statistics of Rodin proof tactics

HOL-EventB:

• faster version of ebsimp, called ebsimp'
• axe, a smart combination of simp, clarify, safe, smt, metis, auto, and force
• tuning
• refactoring of EventB
• cleanup of EventB: added missing theorems stating that EventB constitutes a model of Event-B's main theory.
• changed the notation "x..y" to "x. .y", as the notation "x..y" is in conflict with, e.g., {x..y}.

Version 0.4.0

Rodin Plug-ins:

• infrastructure for creating proof statistics with "isabelle usedir"
• Export information about the origin of hypotheses and goals.
• Export information about the underlying refines / sees / extends graph.

HOL-EventB:

• an attribute unlifted for forward application of ebsimp
• Integrated Gudmund Grov's Formula_Origin theory, which stores the origin of a formula.
• Tuning.
• Fixed a parse problem with <+ and .<+..
• logging facilities
• a command "is_finished" that determines whether a proof is finished
• a command "timed_apply" -- a time bounded version of apply

Version 0.3.0

Rodin Plug-ins:

• translation avoids name clashes with predefined constants
• introduce auxiliary definitions to speed up parsing in Isabelle
• improved proof skeletons
• infrastructure for predicate variables

HOL-EventB

• fixed pretty print problems with .>. and .\<ge>.
• The method ebpost no longer uses assumptions in simplification to avoid simplifier loops.

Version 0.2.0

Rodin Plug-ins:

• Avoid duplication of selected hypotheses: hypotheses are now partitioned into the categories selected, deselected, and hidden. Formerly, selected hypotheses appeared both in the categories selected and visible.
• documentation
• implemented a proof command that allows one to export the current sequent of a proof attempt
• success message after export
• Export of proof obligation can now be interrupted (granularity: proof obligation).
• display progress information during export
• implemented the infrastructure to export the sources of predicates and proof obligations

HOL-EventB:

• Reorganized IsaMakefile.

Version 0.1.0

Rodin Plug-ins:

• initial version

HOL-EventB:

• Avoid exponential blow-up by iterated bfunimage.
• Fixed a bug in ebpre split that allowed for split on variables with assm x = \<bullet>.
• Bottom up translation (can still be improved) in ebpre.
• Translate set comprehensions to collect when possible.
• Tuning:
  • iff rules for tfun, pfun, etc.
  • don't unfold functional, injective, funimg
• Beautify structure of WD-conditions of partial operators (e.g., choice).
  • F phi = not(WD phi --> phi)
• Refactoring translation rules for If
• Refactoring translation rules for brestrict, add T/F rules
• Systematically check for expanding rules in ebtranssimp1, use let
• Beautify precondition solving lemmas for partial operators
• Make D an abbreviation.