Difference between revisions of "Export to Isabelle"

From Event-B
Jump to: navigation, search
m
m
Line 13: Line 13:
  
 
The '''EventB Isabelle theory''' introduces Event-B's operators and binders and some proof tactics.
 
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_*/HOL-EventB*.zip".
+
It is shipped with the plug-in and can be found in the location "${update installation path}/features/ch.ethz.infk.isabelle.feature*/HOL-EventB*.zip".
  
 
=Usage=
 
=Usage=

Revision as of 10:16, 10 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 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*/HOL-EventB*.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