|
|
| (12 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*/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.2.0====
| |
| =====Plug-in:=====
| |
| * 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====
| |
| =====Plug-in:=====
| |
| * 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.
| |
