|
|
| (15 intermediate revisions by 2 users not shown) |
| Line 1: |
Line 1: |
| The "Export to Isabelle" plug-in allows users to export proof obligations and sequents to Isabelle/HOL.
| | #REDIRECT [[Isabelle for Rodin]] |
| 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 [ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf].
| |
| | |
| =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
| |
