Export to Isabelle

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*/HOL-EventB*.tgz".

Prerequisites

To process the generated theories, an installation of 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.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.