Difference between pages "Rodin Proof Tactics" and "Theory Plug-in"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Son
 
(Add to Theory Plug-in category)
 
Line 1: Line 1:
This page contains descriptions of the available proof tactics within the RODIN Platform.
+
Return to [[Rodin Plug-ins]]
  
For each tactic, the descriptions is as follows:
+
See also [[Theory Release History]]
  
* '''Description''': A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
+
The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities.
  
* '''Additional details''': Details explanation of the tactic, when it is applicable, give the associated proof rule.
+
===Motivation===
 +
Up to Rodin v2.0, the mathematical language used in Event-B has been fixed. As such, it was not possible to define reusable polymorphic operators. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the Event-B language lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator (which was present in classical B mathematical language) and the bag operator.
  
* '''ID''': An unique ID associated with the tactic.
+
In Rodin v2.0, support for customised syntactic symbols was introduced. The Theory plug-in, as a result, evolved from being just a component to define rewrite rules to a versatile platform to define and validate proof and language extensions.
  
* '''Auto-tactic''': ''No'': the tactic cannot be added as an auto-tactic. ''Yes'': the tactic can be added as an auto-tactic. ''Default'': the tactic is a default auto-tactic.
+
The latest Theory plug-in is released for Rodin v2.8.
  
* '''[[The Proving Perspective (Rodin User Manual)#The Automatic Post-tactic|Post-tactic]]''': ''No'': the tactic cannot be added as a post-tactic. ''Yes'': the tactic can be added as a post-tactic. ''Default'': the tactic is a default post-tactic.
+
===Overview===
 +
The Theory plug-in is a Rodin extension that provides the facility to define '''''mathematical extensions''''' as well as '''''prover extensions'''''.
 +
Mathematical extensions are new operator definitions and new datatype definitions and axiomatic definitions. Operator definitions can be expression operators (e.g., ''card'') and predicate operators (e.g., ''finite''). Datatypes extensions can be used to define enumerated datatypes (e.g., ''DIRECTION'') as well as inductive datatypes (e.g., ''Tree''). Axiomatic definitions can be used to define new data types like "REAL".
  
* '''Preference display''': (Optional) If the tactic can be used as an auto-tactic or a post-tactic, information on how the tactic is displayed in the auto-tactic preference or the post-tactic preference.
+
The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, axiomatic definitions, inference and rewrite rules as well as polymorphic theorems. The [http://wiki.event-b.org/images/Theory_Plugin.pdf user manual] provides a guide to developing and using theories.
  
* '''Interactive''': ''No'': the tactic cannot be invoked interactively from the [[The Proving Perspective (Rodin User Manual)|proving interface]]. ''Global'': The tactic can be invoked interactively from the [[The Proving Perspective (Rodin User Manual)#The Proof Control Window|Proof Control View]]. ''Goal'': The tactic can be invoked from the [[The Proving Perspective (Rodin User Manual)#Goal and Selected Hypotheses|Goal view]]. ''Hypothesis'': The tactic can be invoked from the [[The Proving Perspective (Rodin User Manual)#Goal and Selected Hypotheses| Hypothesis view]].  If the tactic can be invoked interactively (i.e. either ''Global'', ''Goal'' or ''Hypothesis''), more information about how this could be done will be given. Note that since the '''Post-tactics''' can be launched manually, any tactics that can be included in the post-tactic in principle can be invoked interactively via the post-tactic. Here ''No'' only means that there is no separate invocation for this specific tactic.
+
=== Installation & Update ===
  
* '''Proving interface display''': Example(s) on how applications of this tactic can be seen from the [[The Proving Perspective (Rodin User Manual)|proving interface]] of the RODIN Platform.
+
The installation or update for the Theory plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates) under the category "Modelling Extensions". Like always, after the installation, restarting Rodin is recommended.
  
== True Goal ==
+
===User Manual===
* '''Description''': Discharges any sequent whose goal is '⊤' (logical true).
+
The user manual is available here: [http://wiki.event-b.org/images/Theory_Plugin.pdf Theory User Manual]. Below is the presentation of the sequence theory which its description can be found in the user manual:
  
* '''Additional details''': {{InfRule|HYP|<math>\frac{}{\mathsf{H} \;\;\vdash \;\; \btrue}</math>}}
+
[[image:SeqTheory.png|center|thumb|1500px|'''Theory of Sequence''']]
  
* '''ID''': org.eventb.core.seqprover.trueGoalTac
+
===Standard Library===
 +
In this section, you find a set of standard theories and some models using some of these theories.  
  
* '''Auto-tactic''': ''Default''
+
The standard library of the theories is available to download:
 +
[https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.1.zip/download here] for Rodin2.8 and
 +
[https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.2.zip/download here] for Rodin3.1.
 +
This library includes:
 +
* BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.
 +
* RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.
 +
* RealTheory project: including theory of Real.
  
* '''Post-tactic''': ''Default''
+
Also it includes three simple Event-B models that use some of the theories:
 +
* Data project: using SUMandPRODUCT theory
 +
* Queue project: using Seq theory
 +
* SimpleNetwork project: using closure theory
  
* '''Preference display''': True Goal (Discharge)
+
In order to keep the POs discharged, you need to install "Atelier B provers" as well.
  
* '''Interactive''': ''No''
+
===Capabilities===
 +
The Theory plug-in has the following capabilities:
  
* '''Proving interface display''': goal
+
* Theory Definition:
 +
** Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
 +
** Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is ''card''. A predicate operator is one that "returns" a predicate, an example existing predicate operator is ''finite''.
 +
** Definition of axiomatic definitions: axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms.
 +
** Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
 +
** Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
 +
** Definition of polymorphic theorems: theorems can be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
 +
** Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
 +
*Theory Deployment: this step signifies that a theory is ready for use. Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.
 +
Once a theory has been deployed to its designated project, all its extensions (mathematical and prover extensions) can be used in models.
  
[[Image:TrueGoalExp1.png]]
+
===Insider Look===
 +
The Theory plug-in partially satisfies the requirements outlined in the following document:
 +
* [http://deploy-eprints.ecs.soton.ac.uk/80/ Abrial, Jean-Raymond and Butler, Michael and Schmalz, Matthias and Hallerstede, Stefan and Voisin, Laurent. Mathematical Extensions Proposal]
  
== False Hypothesis ==
+
A more accurate description of the implemented functionalities of the plug-in can be found in the following document:
* '''Description''': Discharges any sequent containing a '⊥' hypothesis
+
* [http://deploy-eprints.ecs.soton.ac.uk/251/ Michael Butler, Issam Maamria. Mathematical Extensions Summary]
  
* '''Additional details''': {{InfRule|FALSE_HYP|<math>\frac{}{\mathsf{H}, \bfalse \;\;\vdash \;\; \mathit{P}}</math>}}
+
The following two papers describe rewriting and well-definedness issues that has to be accounted for:
  
* '''ID''': org.eventb.core.seqprover.falseHypTac
+
* [http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.]
 +
* [http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.]
  
* '''Auto-tactic''': ''Default''
 
  
* '''Post-tactic''': ''Default''
+
[[Category:Plugin]]
 
+
[[Category:User documentation]]
* '''Preference display''': False Hypothesis (Discharge)
+
[[Category:Proof]]
 
+
[[Category:Theory Plug-in]]
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': ⊥ hyp
 
 
 
[[Image: FalseHypExp1.png]]
 
 
 
== Goal in Hypotheses ==
 
* '''Description''': Discharges any sequent whose goal is contained in its hypotheses
 
 
 
* '''ID''': org.eventb.core.seqprover.goalInHypTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Goal in Hypotheses (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': hyp
 
 
 
[[Image: GoalInHypExp1.png]]
 
 
 
== Goal Disjunct in Hypothesis ==
 
* '''Description''': Discharges any sequent whose goal is a disjunction and one of whose disjuncts is present in the hypotheses.
 
 
 
* '''ID''': org.eventb.core.seqprover.goalDisjInHypTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Goal Disjunct in Hypotheses (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': ∨ goal in hyp
 
 
 
[[Image: GoalDisjInHypExp1.png]]
 
 
 
== Functional Goal ==
 
* '''Description''': Tries to discharge a sequent whose goal states that an expression is a function (i.e. f ∈ T1 ⇸ T2, where T1 and T2 are type expressions).
 
 
 
* '''Additional details''': The sequent is discharged if there is a hypothesis specifying that f is a function of any kind (i.e. partial function, total function, partial injection, total injection, partial surjection,  total surjection, bijection). More information about type expressions in Event-B is in the [[FAQ#What are type expressions in Event-B?|FAQ]] page.
 
 
 
* '''ID''': org.eventb.core.seqprover.funGoalTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Functional Goal (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': functional goal
 
 
 
[[Image:FunctionalGoalExp1.png]]
 
 
 
== Simplification Rewriter ==
 
* '''Description''': Tries to simplify all predicates in a sequent using pre-defined simplification rewriting rules.
 
 
 
* '''Additional details''': The list of rewriting rules are in the following page [[All Rewrite Rules | http://wiki.event-b.org/index.php/All_Rewrite_Rules]], which are marked as ''Automatic''.
 
 
 
* '''ID''': org.eventb.core.seqprover.autoRewriteTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Simplification Rewriter (Simplify)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': simplification rewrites
 
 
 
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.  There are 3 rewritings have been done as follows.
 
 
 
<math>
 
\begin{array}{rcl}
 
a + 0  & \Longrightarrow & a \\
 
a = a & \Longrightarrow & \btrue \\
 
c * 1 & \Longrightarrow & c \\
 
\end{array}
 
</math>
 
 
 
Note that <math>\btrue</math> hypothesis is always ''dropped'' in the RODIN Platform.
 
 
 
Before [[Image:SimplifcationRewritesExp1.png]]
 
 
 
After [[Image:SimplifcationRewritesExp2.png]]
 
 
 
== Type Rewriter ==
 
* '''Description''': Simplifies predicates containing type expressions such as E ∈ T to ⊤ and T = ∅ to ⊥.
 
 
 
* '''Additional details''': More information about type expressions in Event-B is in the [[FAQ#What are type expressions in Event-B?|FAQ]] page.
 
 
 
* '''ID''': org.eventb.core.seqprover.typeRewriteTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Type Rewriter (Simplify)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': type rewrites
 
 
 
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.
 
 
 
Before [[Image: TypeRewritesExp1.png]]
 
 
 
After [[Image: TypeRewritesExp2.png]]
 
 
 
== Implication Goal ==
 
* '''Description''': Simplifies any sequent with an implicative goal by adding the left hand side of the implication to the hypotheses and making its right hand side the new goal.
 
 
 
* '''ID''': org.eventb.core.seqprover.impGoalTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Implicative Goal (Simplify)
 
 
 
* '''Interactive''': ''Goal''. The <math>\limp</math> symbol in the implicative goal is <font color=red>''redden''</font>. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Deduction''.
 
 
 
[[Image: ImpGoalInteractive1.png]]
 
 
 
* '''Proving interface display''': ⇒ goal
 
 
 
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.
 
 
 
Before [[Image: ImpGoalExp1.png]]
 
 
 
After [[Image: ImpGoalExp2.png]]
 
 
 
== For-all Goal ==
 
* '''Description''': Simplifies any sequent with a universally quantified goal by freeing all its bound variables.
 
 
 
* '''Additional details''': The bound variables will be renaming accordingly to avoid name collision.
 
 
 
* '''ID''': org.eventb.core.seqprover.forallGoalTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Yes''
 
 
 
* '''Preference display''': For-all Goal (Simplify)
 
 
 
* '''Interactive''': ''Goal''. The  symbol <math>\forall</math> in the universal quantified goal is <font color=red>''redden''</font>. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Forall instantiation''.
 
 
 
[[Image: ForallGoalInteractive1.png]]
 
 
 
* '''Proving interface display''': ∀ goal (frees ''list-of-bounded-identifiers'')
 
 
 
The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.  There is no renaming of the bound variable.
 
 
 
Before [[Image: ForallGoalExp1.png]]
 
 
 
After [[Image: ForallGoalExp2.png]]
 
 
 
The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable <math>x</math> is not renamed, but the bound variable <math>z</math> is renamed to <math>z0</math> to avoid capture of the existing variable <math>z</math>.
 
 
 
Before [[Image: ForallGoalExp3.png]]
 
 
 
After [[Image: ForallGoalExp4.png]]
 
 
 
== Exists Hypothesis ==
 
* '''Description''': In automatic mode (as an auto-tactic or post-tactic), this tactic simplifies any sequent containing existentially quantified hypotheses by freeing their bound variables. In interactive mode, only the selected hypothesis is simplified by freeing its bound variables.
 
 
 
* '''Additional details''': The bound variables will be renaming if necessary to avoid name collision. After freeing their bound variables, if the resulting predicate is a conjunction then it is split into several hypotheses.
 
 
 
* '''ID''': org.eventb.core.seqprover.existHypTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Exists Hypotheses (Simplify)
 
 
 
* '''Interactive''': ''Hypothesis''. The symbol <math>\exists</math> in the existential quantified hypothesis is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Free existential variables''.
 
 
 
[[Image: ExistsHypInteractive1.png]]
 
 
 
* '''Proving interface display''':
 
 
 
The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. There is no renaming of the bound variable.
 
 
 
Before [[Image: ExistHypExp1.png]]
 
 
 
After [[Image: ExistHypExp2.png]]
 
 
 
The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable x is not renamed, but the bound variable z is renamed to z0 to avoid capture of the existing variable z.
 
 
 
Before [[Image: ExistHypExp3.png]]
 
 
 
After [[Image: ExistHypExp4.png]]
 
 
 
== Find Contradictory Hypothesis ==
 
* '''Description''': Discharges a sequent by finding contradictory hypotheses, i.e. <math>P</math> and <math>\neg P </math>.
 
 
 
* '''Additional details''': This tactic tries to find a contradiction using each selected hypothesis that is a negation.
 
 
 
* '''ID''': org.eventb.core.seqprover.findContrHypsTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Find Contradictory Hypotheses (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': ct in hyps (''the negated hypothesis'')
 
 
 
[[Image: FindContrHypsExp1.png]]
 
 
 
== Use Equality Hypothesis ==
 
* '''Description''': Simplifies a sequent by rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between a free variable and an expression that does not contain the free variable. The used equality remains in the selected hypotheses to be used again.
 
 
 
* '''Additional details''': Each application of the tactic take only one equality hypothesis into account. If there are several equality hypotheses, they require several applications of the tactic. Moreover, in the case where there are several equality hypotheses, the choice of which hypothesis will be chosen is non-deterministic.  This tactic behaves as [[#Use Equality Hypothesis from Left to Right]] or [[#Use Equality Hypothesis from Right to Left]] depending on if the free variable is on the left or on the right of the equality.
 
 
 
* '''ID''': org.eventb.core.seqprover.eqHypTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display'': Use Equals Hypotheses (Simplify)
 
 
 
* '''Interactive''': ''Hypothesis''. See [[#Use Equality Hypothesis from Left to Right]] and [[#Use Equality Hypothesis from Right to Left]]
 
 
 
* '''Proving interface display''': eh (''the equal hypothesis'') in the case where the free variable is on the left-hand side or he (''the equal hypothesis'') in the case where the free variable is on the right-hand side.
 
 
 
The  example below shows the screen-shots of the step before the application of the tactic, the step after the first application of the tactic with hypothesis <math>x = y + 1</math> and the step just after the second application of the tactic with hypothesis <math>1 = y</math>.
 
 
 
Before [[Image:UseEqualityHypExp1.png]]
 
 
 
After the first application [[Image:UseEqualityHypExp2.png]]
 
 
 
After the second application [[Image:UseEqualityHypExp3.png]]
 
 
 
== Use Equality Hypothesis from Left to Right ==
 
 
 
* '''Description''': Rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between two expressions. The used equality remains in the selected hypotheses to be used again.
 
 
 
* '''ID''':
 
 
 
* '''Auto-tactic''': See [[#Use Equality Hypothesis]]
 
 
 
* '''Post-tactic''': See [[#Use Equality Hypothesis]]
 
 
 
* '''Interactive''': ''Hypothesis''
 
 
 
* '''Proving interface display''':
 
 
 
== Shrink Implicative Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Shrink Enumerated Set ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Implicative Hypothesis with Conjunctive RHS ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Implicative Hypothesis with Disjunctive LHS ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Conjunctive Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Clarify Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Functional Overriding in Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Functional Overriding in Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Partition Rewriter ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== One-Point Rule in Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== One-Point Rule in Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Bounded Goal with Finite Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Falsify Goal ==
 
 
 
== conjI ==
 
 
 
== allI ==
 
 
 
== exI ==
 
 
 
== Remove Negation ==
 
 
 
== Review ==
 
 
 
== Proof by cases ==
 
 
 
== Add Hypothesis ==
 
 
 
== Abstract Expression ==
 
 
 
== Automatic Prover ==
 
 
 
== Post tactic ==
 
 
 
== Lasoo ==
 
 
 
== Back Tracking ==
 
 
 
== Prune ==
 
 
 
== Search Hypothesis ==
 
 
 
== Cache Hypothesis ==
 
 
 
== Previous ==
 
 
 
== Next ==
 
 
 
== Information ==
 
 
 
== Falsify Hypothesis ==
 
 
 
== Modus Ponens ==
 
 
 
== conjE ==
 
 
 
== disjE ==
 
 
 
== allE ==
 
 
 
== exE ==
 
 
 
 
 
 
 
== Double Implication Hypothesis ==
 
 
 
== cont Implication Hypothesis ==
 
 
 
== Functional Overriding ==
 
 
 
 
 
 
 
== Modus Tollens ==
 
 
 
== Remove Membership ==
 
 
 
== Remove Inclusion ==
 
 
 
== Remove Strict-Inclusion ==
 
 
 
== Inclusion Set Minus Right ==
 
 
 
== Remove Inclusion Universal ==
 
 
 
== Implication Introduction ==
 
 
 
== Disjunction to Implication ==
 
 
 
== Forall Modus Ponens ==
 
 
 
== Next Pending Sub-goal ==
 
 
 
== Next Reviewed Sub-goal ==
 
 
 
== impAndHyp ==
 
 
 
== impAndGoal ==
 
 
 
== impOrHyp ==
 
 
 
== impOrGoal ==
 
 
 
== relImgUnionRight ==
 
 
 
== relImgUnionLeft ==
 
 
 
== Set Equality ==
 
 
 
== Equivalent ==
 
 
 
== Functional Intersection Image ==
 
 
 
== Functional Set Minus Image ==
 
 
 
== Functional Singleton Image ==
 
 
 
== Converse Relation ==
 
 
 
== Domain Distribution to the Left ==
 
 
 
== Domain Distribution to the Right ==
 
 
 
== Range Distribution to the Left ==
 
 
 
== Range Distribution to the Right ==
 
 
 
== Set Minus ==
 
 
 
== Conjunction and Disjunction Distribution ==
 
 
 
== Union Conjunction Distribution ==
 
 
 
== compUnionDist ==
 
 
 
== Domain/Range Union Distribution ==
 
 
 
== Relational Overriding ==
 
 
 
== Composition Image ==
 
 
 
== Domain Composition ==
 
 
 
== Range Composition ==
 
 
 
== Functional Composition Image ==
 
 
 
== Finite Set in Goal ==
 
 
 
== Finite Intersection in Goal ==
 
 
 
== Finite Set Minus in Goal ==
 
 
 
== Finite Relation in Goal ==
 
 
 
== Finite Relation Image in Goal ==
 
 
 
== Finite Domain in Goal ==
 
 
 
== Finite Range in Goal ==
 
 
 
== Finite Function in Goal ==
 
 
 
== Finite Function Converse in Goal ==
 
 
 
== Finite Functional Relational Image in Goal ==
 
 
 
== Finite Functional Range in Goal ==
 
 
 
== Finite Functional Domain in Goal ==
 
 
 
== Finite Minimum in Goal ==
 
 
 
== Finite Maximum in Goal ==
 
 
 
== Finite Negative in Goal ==
 
 
 
== Finite Positive in Goal ==
 
 
 
== Cardinality Comparison in Goal ==
 
 
 
== Cardinality Up to ==
 
 
 
== Partition Rewrite ==
 
 
 
== Arithmetic Rewrite ==
 
 
 
== Total Domain in Hypothesis / Goal ==
 

Latest revision as of 14:53, 14 June 2021

Return to Rodin Plug-ins

See also Theory Release History

The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities.

Motivation

Up to Rodin v2.0, the mathematical language used in Event-B has been fixed. As such, it was not possible to define reusable polymorphic operators. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the Event-B language lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator (which was present in classical B mathematical language) and the bag operator.

In Rodin v2.0, support for customised syntactic symbols was introduced. The Theory plug-in, as a result, evolved from being just a component to define rewrite rules to a versatile platform to define and validate proof and language extensions.

The latest Theory plug-in is released for Rodin v2.8.

Overview

The Theory plug-in is a Rodin extension that provides the facility to define mathematical extensions as well as prover extensions. Mathematical extensions are new operator definitions and new datatype definitions and axiomatic definitions. Operator definitions can be expression operators (e.g., card) and predicate operators (e.g., finite). Datatypes extensions can be used to define enumerated datatypes (e.g., DIRECTION) as well as inductive datatypes (e.g., Tree). Axiomatic definitions can be used to define new data types like "REAL".

The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, axiomatic definitions, inference and rewrite rules as well as polymorphic theorems. The user manual provides a guide to developing and using theories.

Installation & Update

The installation or update for the Theory plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates) under the category "Modelling Extensions". Like always, after the installation, restarting Rodin is recommended.

User Manual

The user manual is available here: Theory User Manual. Below is the presentation of the sequence theory which its description can be found in the user manual:

Theory of Sequence

Standard Library

In this section, you find a set of standard theories and some models using some of these theories.

The standard library of the theories is available to download:

here for Rodin2.8 and
here for Rodin3.1. 

This library includes:

  • BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.
  • RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.
  • RealTheory project: including theory of Real.

Also it includes three simple Event-B models that use some of the theories:

  • Data project: using SUMandPRODUCT theory
  • Queue project: using Seq theory
  • SimpleNetwork project: using closure theory

In order to keep the POs discharged, you need to install "Atelier B provers" as well.

Capabilities

The Theory plug-in has the following capabilities:

  • Theory Definition:
    • Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
    • Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is card. A predicate operator is one that "returns" a predicate, an example existing predicate operator is finite.
    • Definition of axiomatic definitions: axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms.
    • Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
    • Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
    • Definition of polymorphic theorems: theorems can be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
    • Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
  • Theory Deployment: this step signifies that a theory is ready for use. Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.

Once a theory has been deployed to its designated project, all its extensions (mathematical and prover extensions) can be used in models.

Insider Look

The Theory plug-in partially satisfies the requirements outlined in the following document:

A more accurate description of the implemented functionalities of the plug-in can be found in the following document:

The following two papers describe rewriting and well-definedness issues that has to be accounted for: