Difference between pages "Rodin Plug-ins" and "Rodin Proof Tactics"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Rivera
(→‎Code Generation: added EventB2SQL)
 
imported>Son
 
Line 1: Line 1:
''For developer support, see [[Rodin Developer Support]]''
+
This page contains descriptions of the available proof tactics within the RODIN Platform.
  
== Rodin Plug-in Documentation ==
+
For each tactic, the descriptions is as follows:
  
=== Modelling ===
+
* '''Description''': A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
 
* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
 
* [[Records_Extension|Records]] provide structured types for Event-B.
 
* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.
 
* [[Parallel Composition using Event-B]] allows the composition of machines through events for Event-B.
 
* [[Decomposition Plug-in User Guide|Decomposition Plug-in]] allows the decomposition of Event-B machines/contexts (shared variables (A-style) and shared events decomposition (B-style))
 
* [[Refactoring Framework]] allows the refactoring of elements that are part of file (and also on related files).
 
* [[Rose (Structured) Editor]] a model structured editor.
 
* [[Flows]] plug-in allows the addition of control flow to a machine.
 
* [[Image:Mlogo_big.png|40px]] [[Modularisation Plug-in]] provides a mechanism for constructing and proving modular developments.
 
* [[Mode/FT Views]] plug-in brings modelling of modal and fault tolerance features.
 
* [[Team-based development]] enables Event-B models to be stored in a shared repository (e.g. SVN).
 
* [[Event-B Qualitative Probability User Guide | Qualitative Probability]] provides supports for reasoning about termination with probability 1 (almost-certain termination).
 
  
=== Animation ===
+
* '''Additional details''': (Optional) Details explanation of the tactic.
* [[Image:prob_logo_small.png|16px]] [[ProB]] is an animator and model checker for the B-Method,
 
* [[Image:AnimB.png|50px]] [[AnimB]] is an animator for the Rodin platform,
 
* [[UML-B - Statemachine Animation]] provides an animation (using Pro-B) of UML-B State-machines,
 
  
=== Visualization ===
+
* '''ID''': An unique ID associated with the tactic.
* [[Image:bms_logo_small.png|16px]] [[BMotion Studio]] a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization.
 
  
=== Documentation ===
+
* '''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.
* [[Image:ProR_logo.png|32px]] [[ProR]] supports integration of natural language requirements and Event-B models.
 
* [[B2Latex]] allows to typeset an event-B model with latex,
 
  
=== Theory and Proof ===
+
* '''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.
* [[Isabelle for Rodin]]: Prove proof obligations with Isabelle/HOL. Export proof obligations to Isabelle/HOL theories.
 
* [[Theory Plug-in|Theory Plug-in]] provides capabilities to extend the Event-B mathematical language and the Rodin proving infrastructure.
 
* [[Proof Purger Interface|Proof Purger]] offers to delete unused proofs.
 
* [[Proof Skeleton View]] displays the skeleton of existing proofs.
 
* [[SMT Plug-in]] provides interface for SMT solvers.  
 
* [[Relevance Filter Plug-in]] Uses heuristics to filter hypotheses shown to the prover
 
  
=== Code Generation ===
+
* '''Preference display''': Information on how an application of the tactic is displayed in the auto-tactic preference or the post-tactic preference.
* [http://poporo.uma.pt/favas/EventB2Java.html EventB2Java] generates JML-specified Java implementations of Event-B models. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
 
* [http://poporo.uma.pt/favas/EventB2JML.html EventB2JML] translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
 
* [http://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.
 
* [http://users.dickinson.edu/~wahlst/eventb2sql/eventb2sql.html EventB2SQL] translates Event-B machines to Java implementations that make the state of a machine persistent by storing it in a database.
 
* [http://eb2all.loria.fr/ EB2ALL] (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.
 
* [[Code Generation|Tasking Event-B]] supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.
 
* [[B2C plugin|B2C]] translates Event-B models to C source code, which may then be compiled using external C development tools.
 
* [http://eventb-to-vhdl.tk/ EHDL] The plug-in enables [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6037401 VHDL code generation] from formal Event-B models automatically.
 
  
=== Experimental ===
+
* '''Interactive''': ''No'': the tactic cannot be invoked interactively. ''Global'': The tactic can be invoked from the Proof Control. ''Goal'': The tactic can be invoked from the goal view. ''Hypothesis'': The tactic can be invoked from the 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.
* [[Group refinement plugin|Group Refinement]] changes the set of refinement laws for one refinement step to facilitate a case of atomicity refinement.
 
* [[Model Critic]] is an extension using the Epsilon scripting language to analyse Event-B models
 
* [[Feature Composition Plug-in]] allows the composition of Event-B features (machines|contexts) and helps the user in resolving conflicts before composition.
 
* [[Feature Modelling Tool]] (prototype) can be used to build feature models for product lines and configure these to generate product line members.
 
* [[Pattern]] allows the reusing of existing models within a development in order to save the modelling and proving effort.
 
* [[Image:Project diagram icon s.png]] [[Project Diagram]] displays the diagram of a Rodin project.
 
* [[MBT_plugin|MBT plugin]] can be used to generate test sequences covering the events of an Event-B model.
 
* [[Transformation patterns]] allow writing and running transformation scripts in EOL over Event-B models.
 
  
== Rodin Plug-in Tutorials ==
+
* '''Proving interface display''': Example(s) on how an application of this tactic can be seen from the proving interface of the RODIN Platform.
* [[UML-B Tutorial]]
 
* [[Requirements Tutorial]],
 
* [[AnimB Flash Tutorial|Flash Animation Tutorial]] with animB and Adobe CS3.
 
* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial]
 
== Tips & Tricks ==
 
  
* [[Installing external plug-ins manually]]
+
== True Goal ==
 +
* '''Description''': Discharges any sequent whose goal is '⊤' (logical true).
  
[[Category:User documentation]]
+
* '''ID''': org.eventb.core.seqprover.trueGoalTac
[[Category:Plugin]]
+
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': True Goal (Discharge)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': ⊤ goal
 +
 
 +
[[Image:TrueGoalExp1.png]]
 +
 
 +
== False Hypothesis ==
 +
* '''Description''': Discharges any sequent containing a '⊥' hypothesis
 +
 
 +
* '''ID''': org.eventb.core.seqprover.falseHypTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': False Hypothesis (Discharge)
 +
 
 +
* '''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).
 +
 
 +
* '''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]].
 +
 
 +
* '''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''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== For-all Goal ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Exists Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Find Contradictory Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Use Equality Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== 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 ==
 +
 
 +
== eq1 ==
 +
 
 +
== Double Implication Hypothesis ==
 +
 
 +
== cont Implication Hypothesis ==
 +
 
 +
== Functional Overriding ==
 +
 
 +
== Equality ==
 +
 
 +
== 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 ==

Revision as of 13:43, 9 March 2010

This page contains descriptions of the available proof tactics within the RODIN Platform.

For each tactic, the descriptions is as follows:

  • Description: A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
  • Additional details: (Optional) Details explanation of the tactic.
  • ID: An unique ID associated with the tactic.
  • 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.
  • 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.
  • Preference display: Information on how an application of the tactic is displayed in the auto-tactic preference or the post-tactic preference.
  • Interactive: No: the tactic cannot be invoked interactively. Global: The tactic can be invoked from the Proof Control. Goal: The tactic can be invoked from the goal view. Hypothesis: The tactic can be invoked from the 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.
  • Proving interface display: Example(s) on how an application of this tactic can be seen from the proving interface of the RODIN Platform.

Contents

True Goal

  • Description: Discharges any sequent whose goal is '⊤' (logical true).
  • ID: org.eventb.core.seqprover.trueGoalTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: True Goal (Discharge)
  • Interactive: No
  • Proving interface display: ⊤ goal

TrueGoalExp1.png

False Hypothesis

  • Description: Discharges any sequent containing a '⊥' hypothesis
  • ID: org.eventb.core.seqprover.falseHypTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: False Hypothesis (Discharge)
  • Interactive: No
  • Proving interface display: ⊥ hyp

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

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

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).
  • ID: org.eventb.core.seqprover.funGoalTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: Functional Goal (Discharge)
  • Interactive: No
  • Proving interface display: functional goal

FunctionalGoalExp1.png

Simplification Rewriter

  • Description: Tries to simplify all predicates in a sequent using pre-defined simplification rewriting rules.
  • 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.


\begin{array}{rcl}
 a + 0  & \Longrightarrow & a \\
 a = a & \Longrightarrow & \btrue \\
 c * 1 & \Longrightarrow & c \\
\end{array}

Note that \btrue hypothesis is always dropped in the RODIN Platform.

Before SimplifcationRewritesExp1.png

After 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.
  • 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 TypeRewritesExp1.png

After TypeRewritesExp2.png

Implication Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

For-all Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Exists Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Find Contradictory Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Use Equality Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

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

eq1

Double Implication Hypothesis

cont Implication Hypothesis

Functional Overriding

Equality

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