Export to Isabelle - Revision history

imported>Wohuai: Redirecting to Isabelle for Rodin

2012-02-25T17:01:21Z

← Older revision		Revision as of 17:01, 25 February 2012
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/releases/2.0.0-beta 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~~]]

imported>Wohuai at 08:59, 24 February 2012

2012-02-24T08:59:00Z

← Older revision		Revision as of 08:59, 24 February 2012
Line 9:		Line 9:

	'''Please make sure that'''		'''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 Scala update site http://download.scala-ide.org/releases/2.0.0-beta appears in the list of available software sites, and
	* the box "contact all update sites during install to find required software" is checked.		* the box "contact all update sites during install to find required software" is checked.

imported>Wohuai at 09:55, 3 February 2012

2012-02-03T09:55:53Z

← Older revision		Revision as of 09:55, 3 February 2012
Line 50:		Line 50:
	* a plug-in for generating statistics of Rodin proof tactics		* a plug-in for generating statistics of Rodin proof tactics

	=====HOL-EventB=====		=====HOL-EventB:=====
	* faster version of ebsimp, called ebsimp'		* faster version of ebsimp, called ebsimp'
	* axe, a smart combination of simp, clarify, safe, smt, metis, auto, and force		* axe, a smart combination of simp, clarify, safe, smt, metis, auto, and force

imported>Wohuai at 09:55, 3 February 2012

2012-02-03T09:55:26Z

← Older revision		Revision as of 09:55, 3 February 2012
Line 43:		Line 43:

	=News=		=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====		====Version 0.4.0====

imported>Mathieu: /* HOL-EventB: */

2011-08-01T07:07:33Z

HOL-EventB:

← Older revision		Revision as of 07:07, 1 August 2011
Line 102:		Line 102:
	* Beautify precondition solving lemmas for partial operators		* Beautify precondition solving lemmas for partial operators
	* Make D an abbreviation.		* Make D an abbreviation.


			[[Category:Plugin]]
			[[Category:User documentation]]

imported>Wohuai at 10:23, 29 June 2011

2011-06-29T10:23:01Z

← Older revision		Revision as of 10:23, 29 June 2011
Line 43:		Line 43:

	=News=		=News=

			====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====		====Version 0.3.0====

imported>Wohuai at 14:37, 8 June 2011

2011-06-08T14:37:37Z

← Older revision		Revision as of 14:37, 8 June 2011
Line 46:		Line 46:
	====Version 0.3.0====		====Version 0.3.0====
	=====Plug-in:=====		=====Plug-in:=====
	* tuning
	* translation avoids name clashes with predefined constants		* translation avoids name clashes with predefined constants
	* introduce auxiliary definitions to speed up parsing in Isabelle		* introduce auxiliary definitions to speed up parsing in Isabelle

imported>Wohuai at 14:10, 23 May 2011

2011-05-23T14:10:45Z

← Older revision		Revision as of 14:10, 23 May 2011
Line 6:		Line 6:
	=Installation=		=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'''.		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'''		'''Please make sure that'''

imported>Wohuai at 07:43, 18 May 2011

2011-05-18T07:43:05Z

← Older revision		Revision as of 07:43, 18 May 2011
Line 54:		Line 54:
	=====HOL-EventB=====		=====HOL-EventB=====
	* fixed pretty print problems with .>. and .\<ge>.		* fixed pretty print problems with .>. and .\<ge>.
	* ebpost no longer uses assumptions in simplification to avoid simplifier loops		* The method ebpost no longer uses assumptions in simplification to avoid simplifier loops.

	====Version 0.2.0====		====Version 0.2.0====

imported>Wohuai at 07:42, 18 May 2011

2011-05-18T07:42:31Z

← Older revision		Revision as of 07:42, 18 May 2011
Line 43:		Line 43:

	=News=		=News=

			====Version 0.3.0====
			=====Plug-in:=====
			* tuning
			* 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>.
			* ebpost no longer uses assumptions in simplification to avoid simplifier loops

	====Version 0.2.0====		====Version 0.2.0====