Export to Isabelle: Difference between revisions
imported>Wohuai No edit summary |
imported>Wohuai No edit summary |
||
| Line 11: | Line 11: | ||
* the Scala update site http://download.scala-ide.org/update-current appears in the list of available software sites, and | * 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. | * the box "contact all update sites during install to find required software" is checked. | ||
The '''EventB Isabelle theory''' introduces Event-B's operators and binders and some proof tactics. | |||
It is shipped with the plug-in and can be found in the location "${update installation path}/features/ch.ethz.infk.isabelle.feature_*/holeb*.zip". | |||
=Usage= | =Usage= | ||
Revision as of 13:27, 9 May 2011
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.
The EventB Isabelle theory introduces Event-B's operators and binders and some proof tactics. It is shipped with the plug-in and can be found in the location "${update installation path}/features/ch.ethz.infk.isabelle.feature_*/holeb*.zip".
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
