Export to Isabelle

The "Export to Isabelle" plug-in allows users to export proof obligations and sequents to Isabelle/HOL. Its main purpose is to help researchers analyse proof obligations in Isabelle; in the long run, it will form the basis of automated proof tactics for Event-B based on Isabelle. The embedding of Event-B's logic in Isabelle/HOL is sound with respect to the semantics described in [1].

Installation

The plug-in can be installed using Rodin's update 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/update-current appears in the list of available software sites, and
• the box "contact all update sites during install to find required software" is checked.

Usage

The plug-in can be used to export proof obligations or the intermediate sequent of a proof attempt.

Exporting Proof Obligations

• 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 files with the proof attempts need to be renamed to the form "*.thy" before Isabelle can process them. Separating proof obligations from proofs makes it easy to update the proof obligations without destroying the proof files.

Exporting the Intermediate Sequent of a Proof Attempt

The proof control provides a button "Export to Isabelle". After pressing the button, the user is prompted for a file name, where the sequent is stored.

News

Version 0.1.0

• initial version