|
|
| (2 intermediate revisions by the same user 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*.tgz".
| |
| | |
| ===Prerequisites===
| |
| To process the generated theories, an installation of [http://isabelle.in.tum.de/download.html Isabelle2011] is required.
| |
| | |
| =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.
| |
| | |
| =Limitations=
| |
| | |
| * Names of variables may clash with names of reserved keywords in Isabelle, which leads to parse errors. Similarly, names of components may clash with the name of some built-in theory of HOL.
| |
| | |
| =News=
| |
| | |
| ====Version 0.5.0====
| |
| =====Plug-in:=====
| |
| * (incompatible) changes in translation, taking changes in HOL/Event-B into account
| |
| * infrastructure for doing the experiments of my PhD thesis
| |
| * a plug-in for generating statistics of Rodin proof tactics
| |
| | |
| =====HOL-EventB=====
| |
| * faster version of ebsimp, called ebsimp'
| |
| * axe, a smart combination of simp, clarify, safe, smt, metis, auto, and force
| |
| * tuning
| |
| * refactoring of EventB
| |
| * cleanup of EventB: added missing theorems stating that EventB constitutes a model of Event-B's main theory.
| |
| * changed the notation "x..y" to "x. .y", as the notation "x..y" is in conflict with, e.g., {x..y}.
| |
| | |
| ====Version 0.4.0====
| |
| =====Plug-in:=====
| |
| * infrastructure for creating proof statistics with "isabelle usedir"
| |
| * Export information about the origin of hypotheses and goals.
| |
| * Export information about the underlying refines / sees / extends graph.
| |
| | |
| =====HOL-EventB:=====
| |
| * an attribute unlifted for forward application of ebsimp
| |
| * Integrated Gudmund Grov's Formula_Origin theory, which stores the origin of a formula.
| |
| * Tuning.
| |
| * Fixed a parse problem with <+ and .<+..
| |
| * logging facilities
| |
| * a command "is_finished" that determines whether a proof is finished
| |
| * a command "timed_apply" -- a time bounded version of apply
| |
| | |
| ====Version 0.3.0====
| |
| =====Plug-in:=====
| |
| * translation avoids name clashes with predefined constants
| |
| * introduce auxiliary definitions to speed up parsing in Isabelle
| |
| * improved proof skeletons
| |
| * infrastructure for predicate variables
| |
| | |
| =====HOL-EventB=====
| |
| * fixed pretty print problems with .>. and .\<ge>.
| |
| * The method ebpost no longer uses assumptions in simplification to avoid simplifier loops.
| |
| | |
| ====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.
| |
| | |
| | |
| [[Category:Plugin]]
| |
| [[Category:User documentation]]
| |
