Difference between revisions of "Rodin Proof Tactics"

From Event-B
Jump to navigationJump to search
imported>Son
imported>Nicolas
m (added todo success failure)
 
(165 intermediate revisions by 3 users not shown)
Line 3: Line 3:
 
For each tactic, the descriptions is as follows:
 
For each tactic, the descriptions is as follows:
  
* '''Display''': How an application of the tactic is displayed in the proof tree, the auto-tactic preference or the post-tactic preference.
+
* '''Description''': A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
  
* '''Description''': A high-level description of the tactic
+
* '''Additional details''': Details explanation of the tactic, when it is applicable, give the associated proof rule. See [[Inference Rules|Inference rules]] list and [[All Rewrite Rules | Rewriting rules]] list.
 +
 
 +
* '''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.
 
* '''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.
+
* '''[[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.
 +
 
 +
* '''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 [[The Proving Perspective (Rodin User Manual)#Preferences for the Post-tactic|post-tactic preference]].
 +
 
 +
* '''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.
 +
 
 +
* '''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.
 +
 
 +
{{TODO|add conditions of success/failure}}
 +
 
 +
== True Goal ==
 +
* '''Description''': Discharges any sequent whose goal is '⊤' (logical true).
 +
 
 +
* '''Additional details''': {{InfRule|TRUE_GOAL|<math>\frac{}{\mathsf{H} \;\;\vdash \;\; \btrue}</math>}}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.trueGoalTac
 +
 
 +
* '''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
 +
 
 +
* '''Additional details''': {{InfRule|FALSE_HYP|<math>\frac{}{\mathsf{H}, \bfalse \;\;\vdash \;\; \mathit{P}}</math>}}
 +
 
 +
* '''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
 +
 
 +
* '''Additional details''': {{InfRule|HYP|<math>\frac{}{\mathsf{H}, \mathit{P} \;\;\vdash \;\; \mathit{P}}</math>}}
 +
 
 +
* '''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.
 +
 
 +
* '''Additional details''': {{InfRule|HYP_OR|<math>\frac{}{\mathsf{H}, \mathit{Q} \;\;\vdash \;\; \mathit{P} \lor \ldots \lor \mathit{Q} \lor \ldots \lor \mathit{R}}</math>}}
 +
 
 +
* '''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. The corresponding proof rule is as follows.
 +
 
 +
{{InfRule|FUN_GOAL|<math>\frac{}{\mathsf{H}, f \in E \; op \; F \;\;\vdash \;\; f \in T_1 \pfun T_2}</math>}}
 +
 
 +
where <math>op</math> is either <math>\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij </math>.
 +
 
 +
* '''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 | rewriting rules]], which are marked as ''Automatic''.
 +
 
 +
The corresponding proof rule is as follows.
 +
 
 +
{{InfRule|SIM|<math>\frac{\mathsf{H}, \mathsf{H^\prime} \;\;\vdash \;\; \mathit{P^\prime}}{\mathsf{H} \;\;\vdash \;\; \mathit{P}}</math>}}
 +
 
 +
where <math>\mathsf{H^\prime}</math> are the set of new hypotheses obtained by rewriting some of the original hypothesis in <math>\mathsf{H}</math>, and <math>\mathit{P}</math> is the rewriting of the original goal <math>\mathit{P}</math>.
 +
 
 +
* '''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.
 +
The rewriting rules are SIMP_TYPE_EQUAL_EMPTY and SIMP_TYPE_IN  in the [[All Rewrite Rules | rewriting rules]] page.
 +
 
 +
The corresponding proof rule is as follows.
 +
 
 +
{{InfRule|SIM|<math>\frac{\mathsf{H}, \mathsf{H^\prime} \;\;\vdash \;\; \mathit{P^\prime}}{\mathsf{H} \;\;\vdash \;\; \mathit{P}}</math>}}
 +
 
 +
where <math>\mathsf{H^\prime}</math> are the set of new hypotheses obtained by rewriting some of the original hypothesis in <math>\mathsf{H}</math>, and <math>\mathit{P}</math> is the rewriting of the original goal <math>\mathit{P}</math>.
 +
 
 +
* '''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.
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|IMP_R|<math>\frac{\mathsf{H}, \mathit{P} \;\;\vdash \;\; \mathit{Q}}{\mathsf{H} \;\;\vdash \;\; \mathit{P} \limp \mathit{Q}}</math>}}
 +
 
 +
* '''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.
 +
 
 +
{{InfRule|ALL_R|<math>\frac{\mathsf{H} \;\;\vdash \;\; \mathit{P(x)}}{\mathsf{H} \;\;\vdash \;\; \forall x \qdot \mathit{P(x)}}</math>}}
 +
 
 +
where <math>x</math> does not appear freely in <math>\mathsf{H}</math>.
 +
 
 +
* '''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.
 +
 
 +
{{InfRule|XST_L|<math>\frac{\mathsf{H}, \mathit{P(x)}, \ldots, \mathit{Q(x)} \;\;\vdash \;\; \mathit{R}}{\mathsf{H}, \exists x \qdot \mathit{P(x)} \land \ldots \land \mathit{Q(x)} \;\;\vdash \;\; \mathit{R}}</math>}}
 +
 
 +
where <math>x</math> does not appear freely in <math>\mathsf{H}</math> and <math>\mathit{R}</math>.
 +
 
 +
* '''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.
 +
 
 +
{{InfRule|CNTR|<math>\frac{}{\mathsf{H}, \mathit{P}, \neg\mathit{P} \;\;\vdash \;\; \mathit{Q}}</math>}}
 +
 
 +
* '''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.
 +
 
 +
{{InfRule|EQL_LR|<math>\frac{\mathsf{H(E)}, \mathit{x} = \mathit{E} \;\;\vdash \;\; \mathit{P(E)}}{\mathsf{H(x)}, \mathit{x} = \mathit{E} \;\;\vdash \;\; \mathit{P(x)}}</math>}}
 +
 
 +
{{InfRule|EQL_RL|<math>\frac{\mathsf{H(E)}, \mathit{E} = \mathit{x} \;\;\vdash \;\; \mathit{P(E)}}{\mathsf{H(x)}, \mathit{E} = \mathit{x} \;\;\vdash \;\; \mathit{P(x)}}</math>}}
 +
 
 +
* '''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''': Simplifies the (visible) implicative hypotheses in a sequent by removing predicates from their left hand sides that are (selected) hypotheses.
 +
 
 +
* '''Additional details''':
 +
{{InfRule|AUTO_MH|<math>\frac{
 +
\textbf{H},\textbf{P},\;\textbf{Q}\limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P},\; \textbf{P} \land  \textbf{Q} \limp \textbf{R}  \;\;\vdash \;\; \textbf{S}}</math>}}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.shrinkImpHypTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference Display''': Shrink Implicative Hypotheses (Simplify)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': auto ImpE
 +
 
 +
Before [[Image: ShrinkImpHypBefore.png]]
 +
 
 +
After [[Image: ShrinkImpHypAfter.png]]
 +
 
 +
== Shrink Enumerated Set ==
 +
* '''Description''': Simplifies (selected) hypotheses of the form e ∈ {a,b,c} to e ∈ {a,c} after finding the hypothesis ¬ e = b.
 +
 
 +
* '''Additional details''': TODO
 +
 
 +
* '''ID''': org.eventb.core.seqprover.shrinkEnumHypTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference Display''': Shrink Enumerated Set (Simplify)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving Interface Display''': negEnum ''<hypotheses names>''
 +
 
 +
Before [[Image: ShrinkEnumHypBefore.png]]
 +
 
 +
After Before [[Image: ShrinkEnumHypAfter.png]]
 +
 
 +
== Implicative Hypothesis with Conjunctive RHS ==
 +
* '''Description''': Simplifies all (selected) hypotheses of the form P ⇒ Q ∧ R into multiple implications P ⇒ Q , P ⇒ R.
 +
 
 +
* '''Additional details''':
 +
{{InfRule|IMP_AND_L|<math>\frac{\textbf{H},\textbf{P} \limp \textbf{Q},  \textbf{P} \limp \textbf{R}\;\;\vdash \;\; \textbf{S}}{\textbf{H},\;\textbf{P} \limp  \textbf{Q} \land \textbf{R}  \;\;\vdash \;\; \textbf{S}}</math>}}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.splitRightConjImpHypTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference Display''': Implicative Hypotheses with Conjunctive RHS (Simplify)
 +
 
 +
* '''Interactive''': ''Hypothesis''
 +
The operator <span style="color:red">⇒</span> is redden in the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Implication with conjunction rewrites''.
 +
 
 +
* '''Proving Interface Display''': ⇒ with ∧ in hyp ''<hypothesis name>''
 +
 
 +
Before [[Image: SplitRightConjImpHypBefore.png]]
 +
 
 +
After [[Image: SplitRightConjImpHypAfter.png]]
 +
 
 +
== Implicative Hypothesis with Disjunctive LHS ==
 +
* '''Description''': Simplifies all (selected) hypotheses of the form P ∨ Q ⇒ R into multiple implications P ⇒ R , Q ⇒ R.
 +
 
 +
* '''Additional details''':
 +
{{InfRule|IMP_OR_L|<math>\frac{
 +
\textbf{H},\textbf{P} \limp \textbf{R},  \textbf{Q} \limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P} \lor  \textbf{Q} \limp \textbf{R}  \;\;\vdash \;\; \textbf{S}}</math>}}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.splitLeftDisjImpHypTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference Display''': Implicative Hypotheses with Disjunctive LHS (Simplify)
 +
 
 +
* '''Interactive''': ''Hypothesis''
 +
The operator <span style="color:red">⇒</span> is redden in the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Implication with disjunction rewrites''.
 +
 
 +
* '''Proving Interface Display''': ⇒ with ∨ in hyp ''<hypothesis name>''
 +
 
 +
Before [[Image: SplitLeftDisjImpHypBefore.png]]
 +
 
 +
After [[Image: SplitLeftDisjImpHypAfter.png]]
 +
 
 +
== Conjunctive Goal ==
 +
* '''Description''': Splits a sequent with a conjunctive goal into multiple subgoals.
 +
 
 +
* '''Additional details''':
 +
{{InfRule|AND_R|<math>\frac{\textbf{H} \; \; \vdash \; \;  \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \;  \textbf{P} \; \land \; \textbf{Q}}</math>}}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.conjGoalTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference display''': Conjunctive Goal (Split)
 +
 
 +
* '''Interactive''': ''Goal''
 +
 
 +
[[Image: ConjGoalInteractive.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: ConjGoalBefore.png]]
 +
 
 +
After [[Image: ConjGoalAfter.png]]
 +
 
 +
== Clarify Goal ==
 +
* '''Description''': Clarifies the goal by repeatedly by:
 +
** splitting conjunctions,
 +
** simplifying implications,
 +
** simplifying universal quantifiers,
 +
** discharging sequents with a true goal, a false hypothesis and where the goal is contained in the hypotheses.
 +
 
 +
* '''Additional details''': This tactic applies a composition of tactics [[#Conjunctive Goal]], [[#Implication Goal]] and [[#For-all Goal]] followed by a looping of tactics [[#True Goal]] and [[#False Hypothesis]].
 +
 
 +
* '''ID''': org.eventb.core.seqprover.clarifyGoalTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference Display''': Clarify Goal (Mixed)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
== Functional Overriding in Goal ==
 +
* '''Description''': TODO
 +
 
 +
* '''Additional details''':
 +
{{InfRule|OV_R|<math>\frac{\textbf{H},\; G \in \dom(g) \;\;\vdash\;\;\textbf{Q}(g(G)) \qquad \textbf{H},\; \neg\, G \in \dom(g) \;\;\vdash\;\;\textbf{Q}((\dom(g) \domsub f)(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl g)(G))}</math>}}
 +
 
 +
{{InfRule|OV_SETENUM_R|<math>\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F)
 +
\qquad \textbf{H},\; \neg\,(G=E)  \;\;\vdash\;\;\textbf{Q}((\{E\}) \domsub f)(G))}{\textbf{H}
 +
\;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G))}</math>}}
 +
where Q is WD strict.
 +
 
 +
These inference rules are applied automatically, repeatedly and recursively.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.funOvrGoalTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''No''
 +
 
 +
* '''Preference Display''': Functional Overriding in Goal (Split)
 +
 
 +
* '''Interactive''': ''Goal''
 +
 
 +
When hovering the redden override operator <span style="color:red"><+</span>, select ''(f<+{E|->F})(G)'' from the drop-down menu. (TODO strange menu item)
 +
 
 +
* '''Proving Interface Display''': ovr in goal
 +
 
 +
Before [[Image: FunOvrGoalBefore.png]]
 +
 
 +
First node after application [[Image: FunOvrGoalAfter1.png]]
 +
 
 +
Second node after application [[Image: FunOvrGoalAfter2.png]]
 +
 
 +
== Functional Overriding in Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''Additional details''':
 +
{{InfRule|OV_L|<math>\frac{\textbf{H},\; G \in \dom(g)  ,\;\textbf{P}(g(G))\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,G \in \dom(g)  ,\;\textbf{P}((\dom(g) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl g)(G)) \;\;\vdash \;\; \textbf{Q}}</math>}}
 +
 
 +
{{InfRule|OV_SETENUM_L|<math>\frac{\textbf{H},\; G=E 
 +
,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(G=E) 
 +
,\;\textbf{P}((\{E\}) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E
 +
\mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}}</math> || where <math>\mathbf{P}</math>}}
 +
where P is WD strict.
 +
 
 +
These inference rules are applied automatically, repeatedly and recursively.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.funOvrHypTac
 +
 
 +
* '''Auto-tactic''': ''Yes''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference Display''': Functional Overriding in Hypothesis (Split)
 +
 
 +
* '''Interactive''': ''Hypothesis''
 +
 
 +
When hovering the redden override operator <span style="color:red"><+</span>, select ''(f<+{E|->F})(G)'' from the drop-down menu. (TODO strange menu item)
 +
 
 +
* '''Proving Interface Display''': ovr in ''<hypothesis name>''
 +
 
 +
Before [[Image: FunOvrHypBefore.png]]
 +
 
 +
First node after application [[Image: FunOvrHypAfter1.png]]
 +
 
 +
Second node after application [[Image: FunOvrHypAfter2.png]]
 +
 
 +
== Partition Rewriter ==
 +
* '''Description''': Simplifies all predicates of the form partition(S, ...) into their expanded form in the goal and all visible hypotheses.
 +
 
 +
* '''Additional details''': TODO
 +
 
 +
* '''ID''': org.eventb.core.seqprover.partitionRewriteTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''No''
 +
 
 +
* '''Preference Display''': Partition Rewriter (Simplify)
 +
 
 +
* '''Interactive''': ''Hypothesis, Goal''
 +
 
 +
The predicate <span style="color:red">partition</span> is redden in the goal or the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Rewrites a partition into its definition''.
 +
 
 +
* '''Proving Interface Display''': Partition rewrites in goal / hyp ''<hypothesis name>''
 +
 
 +
Before [[Image: PartitionRewriteBefore.png]]
 +
 
 +
After [[Image: PartitionRewriteAfter.png]]
 +
 
 +
== One-Point Rule in Goal ==
 +
* '''Description''': Applies automatically the OnePointGoal tactic to the goal.
 +
 
 +
* '''Additional details''':
 +
{{InfRule|ONE_POINT_R|<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad  \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H}  \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>}}
 +
 
 +
The rule can be applied with ∀ as well as with ∃.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.onePointGoalTac
 +
 
 +
* '''Auto-tactic''': ''Yes''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference Display''': One Point Rule in Goal (Split)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving Interface Display''': One Point Rule in goal
 +
 
 +
Before [[Image: OnePointGoalBefore.png]]
 +
 
 +
After [[Image: OnePointGoalAfter.png]]
 +
 
 +
== One-Point Rule in Hypothesis ==
 +
* '''Description''': Applies automatically the OnePointHyp tactic to the selected hypotheses.
 +
 
 +
* '''Additional details''':
 +
{{InfRule|ONE_POINT_L|<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad  \textbf{H}, \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} \;\;\vdash \;\; \textbf{G}}{ \textbf{H}, \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R}  \;\;\vdash\;\; \textbf{G}}</math>}}
 +
 
 +
The rule can be applied with ∀ as well as with ∃.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.onePointHypTac
 +
 
 +
* '''Auto-tactic''': ''Yes''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference Display''': One Point Rule in Hypotheses (Split)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving Interface Display''': One Point Rule in ''hypothesis name''
 +
 
 +
Before [[Image: OnePointHypBefore.png]]
 +
 
 +
After [[Image: OnePointHypAfter.png]]
 +
 
 +
== Bounded Goal with Finite Hypothesis ==
 +
* '''Description''': Discharges a sequent whose goal states that an expression E has a lower or a upper bound (e.g. ∃n·(∀x·x ∈ S ⇒ x ≤ n)), when there is an hypothesis that states the finiteness of E (i.e. finite(S)).
 +
 
 +
* '''Additional details''':
 +
{{InfRule|FIN_L_LOWER_BOUND_L|<math>\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}</math>}}
 +
 
 +
{{InfRule|FIN_L_LOWER_BOUND_R|<math>\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \geq n)}</math>}}
 +
 
 +
{{InfRule|FIN_L_UPPER_BOUND_L|<math>\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \geq x)}</math>}}
 +
 
 +
{{InfRule|FIN_L_UPPER_BOUND_R|<math>\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n)}</math>}}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.finiteHypBoundedGoalTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference Display''': Bounded Goal with finite Hypothesis (Discharge)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving Interface Display''': Existence of minimum or maximum in goal with finite hypothesis
 +
 
 +
Before [[Image: FiniteHypBoundedGoalBefore.png]]
 +
 
 +
After [[Image: FiniteHypBoundedGoalAfter.png]]
 +
 
 +
== Falsify Goal ==
 +
 
 +
* '''Description''': Contradicts the goal: the negation of the goal is taken as hypothesis and the goal becomes ''false''.
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|CONTRADICT_R| <math>\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \bfalse}{\textbf{H} \;\;\vdash \;\; \textbf{Q}}</math>}}
 +
 
 +
 
 +
* '''ID''': org.eventb.ui.falsify
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''No''
 +
 
 +
* '''Interactive''': ''Goal''
 +
 
 +
* '''Proving Interface Display''': ''ct''
 +
 
 +
Before [[Image: ctGoalBefore.png]]
 +
 
 +
After [[Image: ctGoalAfter.png]]
 +
 
 +
== Falsify Hypothesis ==
 +
 
 +
* '''Description''': Contradicts an hypothesis: the negation of the goal is taken as hypothesis and the goal becomes the negation of the contradicted hypothesis.
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|CONTRADICT_L| <math>\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \neg\,\textbf{P}}{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math>}}
 +
 
 +
* '''ID''': org.eventb.ui.falsify
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''No''
 +
 
 +
* '''Interactive''': ''Hyp''
 +
 
 +
* '''Proving Interface Display''': ''ct''
 +
 
 +
Before [[Image: ctHypBefore.png]]
 +
 
 +
After [[Image: ctHypAfter.png]]
 +
 
 +
''ct'' has been applied to hypothesis ''card(S)=1''.
 +
 
 +
== conjI ==
 +
 
 +
* '''Description''': Splits a sequent with a conjunctive goal into multiple subgoals.
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|AND_R| <math>\frac{\textbf{H} \; \; \vdash \; \;  \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \;  \textbf{P} \; \land \; \textbf{Q}}</math> }}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.impI
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference Display''': Conjunctive Goal (Split)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving Interface Display''': "Conjunction introduction" for manual application, "''<math>\land</math> goal''" in proof tree
 +
 
 +
Before [[Image: conjIBefore.png]]
 +
 
 +
After [[Image: conjIAfter.png]]
 +
 
 +
== allI ==
 +
 
 +
* '''Description''': Simplifies any sequent with a universally quantified goal by freeing all its bound variables.
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|ALL_R| <math>\frac{\textbf{H}\; \; \vdash \; \;  \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \;  \forall \textbf{x}\, \qdot\, \textbf{P(x)} }</math> }}
 +
 
 +
* '''ID''': org.eventb.core.seqprover.forallGoalTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference Display''': For-all Goal (Simplify)
 +
 
 +
* '''Interactive''': ''Goal''
 +
 
 +
* '''Proving Interface Display''': ''Forall instantiation''
 +
 
 +
Before [[Image: allIBefore.png]]
 +
 
 +
After [[Image: allIAfter.png]]
 +
 
 +
== exI ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: exIBefore.png]]
 +
 
 +
After [[Image: exIAfter.png]]
 +
 
 +
== Remove Negation ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: rnBefore.png]]
 +
 
 +
After [[Image: rnAfter.png]]
 +
 
 +
== Review ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: ReviewBefore.png]]
 +
 
 +
After [[Image: ReviewAfter.png]]
 +
 
 +
== Proof by cases ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: dcBefore.png]]
 +
 
 +
After [[Image: dcAfter.png]]
 +
 
 +
== Add Hypothesis ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: ahBefore.png]]
 +
 
 +
After [[Image: ahAfter.png]]
 +
 
 +
== Abstract Expression ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: aeBefore.png]]
 +
 
 +
After [[Image: aeAfter.png]]
 +
 
 +
== Automatic Prover ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: autoBefore.png]]
 +
 
 +
After [[Image: autoAfter.png]]
 +
 
 +
== Post tactic ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: postBefore.png]]
 +
 
 +
After [[Image: postAfter.png]]
 +
 
 +
== Lasoo ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: LasooBefore.png]]
 +
 
 +
After [[Image: LasooAfter.png]]
 +
 
 +
== Back Tracking ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: BackBefore.png]]
 +
 
 +
After [[Image: BackAfter.png]]
 +
 
 +
== Prune ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: PruneBefore.png]]
 +
 
 +
After [[Image: PruneAfter.png]]
 +
 
 +
== Search Hypothesis ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: SearchBefore.png]]
 +
 
 +
After [[Image: SearchAfter.png]]
 +
 
 +
== Cache Hypothesis ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: CacheBefore.png]]
 +
 
 +
After [[Image: CacheAfter.png]]
 +
 
 +
== Previous ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: PreviousBefore.png]]
 +
 
 +
After [[Image: PreviousAfter.png]]
 +
 
 +
== Next ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: NextBefore.png]]
 +
 
 +
After [[Image: NextAfter.png]]
 +
 
 +
== Information ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: InformationBefore.png]]
 +
 
 +
After [[Image: InformationAfter.png]]
 +
 
 +
== Modus Ponens ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: mpBefore.png]]
 +
 
 +
After [[Image: mpAfter.png]]
 +
 
 +
== conjE ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: conjEBefore.png]]
 +
 
 +
After [[Image: conjEAfter.png]]
 +
 
 +
== disjE ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: disjEBefore.png]]
 +
 
 +
After [[Image: disjEAfter.png]]
 +
 
 +
== allE ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: allEBefore.png]]
 +
 
 +
After [[Image: allEAfter.png]]
 +
 
 +
== exE ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: exEBefore.png]]
 +
 
 +
After [[Image: exEAfter.png]]
 +
 
 +
 
 +
 
 +
== Double Implication Hypothesis ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: dblImpHypBefore.png]]
 +
 
 +
After [[Image: dblImpHypAfter.png]]
 +
 
 +
== cont Implication Hypothesis ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: contImpHypBefore.png]]
 +
 
 +
After [[Image: contImpHypAfter.png]]
 +
 
 +
== Functional Overriding ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: funOvrBefore.png]]
 +
 
 +
After [[Image: funOvrAfter.png]]
 +
 
 +
 
 +
 
 +
== Modus Tollens ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: mtBefore.png]]
 +
 
 +
After [[Image: mtAfter.png]]
 +
 
 +
== Remove Membership ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: rmBefore.png]]
 +
 
 +
After [[Image: rmAfter.png]]
 +
 
 +
== Remove Inclusion ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: riBefore.png]]
 +
 
 +
After [[Image: riAfter.png]]
 +
 
 +
== Remove Strict-Inclusion ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: rsiBefore.png]]
 +
 
 +
After [[Image: rsiAfter.png]]
 +
 
 +
== Inclusion Set Minus Right ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: incSetMinRBefore.png]]
 +
 
 +
After [[Image: incSetMinRAfter.png]]
 +
 
 +
== Remove Inclusion Universal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: riuBefore.png]]
 +
 
 +
After [[Image: riuAfter.png]]
 +
 
 +
== Implication Introduction ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: impIntBefore.png]]
 +
 
 +
After [[Image: impIntAfter.png]]
 +
 
 +
== Disjunction to Implication ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: disj2ImpBefore.png]]
 +
 
 +
After [[Image: disj2ImpAfter.png]]
 +
 
 +
== Forall Modus Ponens ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: fmpBefore.png]]
 +
 
 +
After [[Image: fmpAfter.png]]
 +
 
 +
== Next Pending Sub-goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: NextPendingBefore.png]]
 +
 
 +
After [[Image: NextPendingAfter.png]]
 +
 
 +
== Next Reviewed Sub-goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: NextReviewedBefore.png]]
 +
 
 +
After [[Image: NextReviewedAfter.png]]
 +
 
 +
== impAndHyp ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: impAndHypBefore.png]]
 +
 
 +
After [[Image: impAndHypAfter.png]]
 +
 
 +
== impAndGoal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: impAndGoalBefore.png]]
 +
 
 +
After [[Image: impAndGoalAfter.png]]
 +
 
 +
== impOrHyp ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: impOrHypBefore.png]]
 +
 
 +
After [[Image: impOrHypAfter.png]]
 +
 
 +
== impOrGoal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: impOrGoalBefore.png]]
 +
 
 +
After [[Image: impOrGoalAfter.png]]
 +
 
 +
== relImgUnionRight ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: relImgUnionRightBefore.png]]
 +
 
 +
After [[Image: relImgUnionRightAfter.png]]
 +
 
 +
== relImgUnionLeft ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: relImgUnionLeftBefore.png]]
 +
 
 +
After [[Image: relImgUnionLeftAfter.png]]
 +
 
 +
== Set Equality ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: SetEqBefore.png]]
 +
 
 +
After [[Image: SetEqAfter.png]]
 +
 
 +
== Equivalent ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: EquivalentBefore.png]]
 +
 
 +
After [[Image: EquivalentAfter.png]]
 +
 
 +
== Functional Intersection Image ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: funInterImgBefore.png]]
 +
 
 +
After [[Image: funInterImgAfter.png]]
 +
 
 +
== Functional Set Minus Image ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: funSetMinusImgBefore.png]]
 +
 
 +
After [[Image: funSetMinusImgAfter.png]]
 +
 
 +
== Functional Singleton Image ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: funSingImgBefore.png]]
 +
 
 +
After [[Image: funSingImgAfter.png]]
 +
 
 +
== Converse Relation ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: convRelBefore.png]]
 +
 
 +
After [[Image: convRelAfter.png]]
 +
 
 +
== Domain Distribution to the Left ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: domDistLeftBefore.png]]
 +
 
 +
After [[Image: domDistLeftAfter.png]]
 +
 
 +
== Domain Distribution to the Right ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: domDistRightBefore.png]]
 +
 
 +
After [[Image: domDistRightAfter.png]]
 +
 
 +
== Range Distribution to the Left ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: ranDistLeftBefore.png]]
 +
 
 +
After [[Image: ranDistLeftAfter.png]]
 +
 
 +
== Range Distribution to the Right ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: ranDistRightBefore.png]]
 +
 
 +
After [[Image: ranDistRightAfter.png]]
 +
 
 +
== Set Minus ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: SetMinusBefore.png]]
 +
 
 +
After [[Image: SetMinusAfter.png]]
 +
 
 +
== Conjunction and Disjunction Distribution ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: ConjDisjDistBefore.png]]
 +
 
 +
After [[Image: ConjDisjDistAfter.png]]
 +
 
 +
== Union Conjunction Distribution ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: UnionConjDistBefore.png]]
 +
 
 +
After [[Image: UnionConjDistAfter.png]]
 +
 
 +
== compUnionDist ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: compUnionDistBefore.png]]
 +
 
 +
After [[Image: compUnionDistAfter.png]]
 +
 
 +
== Domain/Range Union Distribution ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: DomRanUnionDistBefore.png]]
 +
 
 +
After [[Image: DomRanUnionDistAfter.png]]
 +
 
 +
== Relational Overriding ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: relOvrBefore.png]]
 +
 
 +
After [[Image: relOvrAfter.png]]
 +
 
 +
== Composition Image ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: compImgBefore.png]]
 +
 
 +
After [[Image: compImgAfter.png]]
 +
 
 +
== Domain Composition ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: domCompBefore.png]]
 +
 
 +
After [[Image: domCompAfter.png]]
 +
 
 +
== Range Composition ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: ranCompBefore.png]]
 +
 
 +
After [[Image: ranCompAfter.png]]
 +
 
 +
== Functional Composition Image ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: funCompImgBefore.png]]
 +
 
 +
After [[Image: funCompImgAfter.png]]
 +
 
 +
== Finite Set in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Intersection in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Set Minus in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Relation in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Relation Image in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Domain in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Range in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Function in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Function Converse in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Functional Relational Image in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Functional Range in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Functional Domain in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Minimum in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Maximum in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Negative in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Finite Positive in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Cardinality Comparison in Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Cardinality Up to ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Partition Rewrite ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Arithmetic Rewrite ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
 +
 
 +
Before [[Image: Before.png]]
 +
 
 +
After [[Image: After.png]]
 +
 
 +
== Total Domain in Hypothesis / Goal ==
 +
 
 +
* '''Description''':
 +
 
 +
* '''Additional details''':
 +
 
 +
{{InfRule|| <math></math> }}
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''':
 +
 
 +
* '''Post-tactic''':
 +
 
 +
* '''Preference Display''':
 +
 
 +
* '''Interactive''':
 +
 
 +
* '''Proving Interface Display''':
  
* '''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.
+
Before [[Image: Before.png]]
  
* '''Example''': Example(s) on how the tactic can be seen from the RODIN Platform.
+
After [[Image: After.png]]

Latest revision as of 17:25, 21 February 2012

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: Details explanation of the tactic, when it is applicable, give the associated proof rule. See Inference rules list and Rewriting rules list.
  • 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: (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.
  • Interactive: No: the tactic cannot be invoked interactively from the proving interface. Global: The tactic can be invoked interactively from the Proof Control View. 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 applications of this tactic can be seen from the proving interface of the RODIN Platform.

TODO: add conditions of success/failure

Contents

True Goal

  • Description: Discharges any sequent whose goal is '⊤' (logical true).
  • Additional details:
\frac{}{\mathsf{H} \;\;\vdash \;\; \btrue} TRUE_GOAL
  • 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
  • Additional details:
\frac{}{\mathsf{H}, \bfalse \;\;\vdash \;\; \mathit{P}} FALSE_HYP
  • 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
  • Additional details:
\frac{}{\mathsf{H}, \mathit{P} \;\;\vdash \;\; \mathit{P}} HYP
  • 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.
  • Additional details:
\frac{}{\mathsf{H}, \mathit{Q} \;\;\vdash \;\; \mathit{P} \lor \ldots \lor \mathit{Q} \lor \ldots \lor \mathit{R}} HYP_OR
  • 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). More information about type expressions in Event-B is in the FAQ page. The corresponding proof rule is as follows.
\frac{}{\mathsf{H}, f \in E \; op \; F \;\;\vdash \;\; f \in T_1 \pfun T_2} FUN_GOAL

where op is either \pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij .

  • 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.
  • Additional details: The list of rewriting rules are in the following page rewriting rules, which are marked as Automatic.

The corresponding proof rule is as follows.

\frac{\mathsf{H}, \mathsf{H^\prime} \;\;\vdash \;\; \mathit{P^\prime}}{\mathsf{H} \;\;\vdash \;\; \mathit{P}} SIM

where \mathsf{H^\prime} are the set of new hypotheses obtained by rewriting some of the original hypothesis in \mathsf{H}, and \mathit{P} is the rewriting of the original goal \mathit{P}.

  • 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 page.

The rewriting rules are SIMP_TYPE_EQUAL_EMPTY and SIMP_TYPE_IN in the rewriting rules page.

The corresponding proof rule is as follows.

\frac{\mathsf{H}, \mathsf{H^\prime} \;\;\vdash \;\; \mathit{P^\prime}}{\mathsf{H} \;\;\vdash \;\; \mathit{P}} SIM

where \mathsf{H^\prime} are the set of new hypotheses obtained by rewriting some of the original hypothesis in \mathsf{H}, and \mathit{P} is the rewriting of the original goal \mathit{P}.

  • 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: 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.
  • Additional details:
\frac{\mathsf{H}, \mathit{P} \;\;\vdash \;\; \mathit{Q}}{\mathsf{H} \;\;\vdash \;\; \mathit{P} \limp \mathit{Q}} IMP_R
  • ID: org.eventb.core.seqprover.impGoalTac
  • Auto-tactic: No
  • Post-tactic: Default
  • Preference display: Implicative Goal (Simplify)
  • Interactive: Goal. The \limp symbol in the implicative goal is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is Deduction.

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 ImpGoalExp1.png

After 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.
\frac{\mathsf{H} \;\;\vdash \;\; \mathit{P(x)}}{\mathsf{H} \;\;\vdash \;\; \forall x \qdot \mathit{P(x)}} ALL_R

where x does not appear freely in \mathsf{H}.

  • ID: org.eventb.core.seqprover.forallGoalTac
  • Auto-tactic: No
  • Post-tactic: Yes
  • Preference display: For-all Goal (Simplify)
  • Interactive: Goal. The symbol \forall in the universal quantified goal is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is Forall instantiation.

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 ForallGoalExp1.png

After 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 x is not renamed, but the bound variable z is renamed to z0 to avoid capture of the existing variable z.

Before ForallGoalExp3.png

After 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.
\frac{\mathsf{H}, \mathit{P(x)}, \ldots, \mathit{Q(x)} \;\;\vdash \;\; \mathit{R}}{\mathsf{H}, \exists x \qdot \mathit{P(x)} \land \ldots \land \mathit{Q(x)} \;\;\vdash \;\; \mathit{R}} XST_L

where x does not appear freely in \mathsf{H} and \mathit{R}.

  • ID: org.eventb.core.seqprover.existHypTac
  • Auto-tactic: No
  • Post-tactic: Default
  • Preference display: Exists Hypotheses (Simplify)
  • Interactive: Hypothesis. The symbol \exists 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.

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 ExistHypExp1.png

After 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 ExistHypExp3.png

After ExistHypExp4.png

Find Contradictory Hypothesis

  • Description: Discharges a sequent by finding contradictory hypotheses, i.e. P and \neg P .
  • Additional details: This tactic tries to find a contradiction using each selected hypothesis that is a negation.
\frac{}{\mathsf{H}, \mathit{P}, \neg\mathit{P} \;\;\vdash \;\; \mathit{Q}} CNTR
  • 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)

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.
\frac{\mathsf{H(E)}, \mathit{x} = \mathit{E} \;\;\vdash \;\; \mathit{P(E)}}{\mathsf{H(x)}, \mathit{x} = \mathit{E} \;\;\vdash \;\; \mathit{P(x)}} EQL_LR
\frac{\mathsf{H(E)}, \mathit{E} = \mathit{x} \;\;\vdash \;\; \mathit{P(E)}}{\mathsf{H(x)}, \mathit{E} = \mathit{x} \;\;\vdash \;\; \mathit{P(x)}} EQL_RL
  • ID: org.eventb.core.seqprover.eqHypTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: Use Equals Hypotheses (Simplify)
  • 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 x = y + 1 and the step just after the second application of the tactic with hypothesis 1 = y.

Before UseEqualityHypExp1.png

After the first application UseEqualityHypExp2.png

After the second application 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:
  • Interactive: Hypothesis
  • Proving interface display:

Shrink Implicative Hypothesis

  • Description: Simplifies the (visible) implicative hypotheses in a sequent by removing predicates from their left hand sides that are (selected) hypotheses.
  • Additional details:
\frac{
\textbf{H},\textbf{P},\;\textbf{Q}\limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P},\; \textbf{P} \land  \textbf{Q} \limp \textbf{R}  \;\;\vdash \;\; \textbf{S}} AUTO_MH
  • ID: org.eventb.core.seqprover.shrinkImpHypTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference Display: Shrink Implicative Hypotheses (Simplify)
  • Interactive: No
  • Proving interface display: auto ImpE

Before ShrinkImpHypBefore.png

After ShrinkImpHypAfter.png

Shrink Enumerated Set

  • Description: Simplifies (selected) hypotheses of the form e ∈ {a,b,c} to e ∈ {a,c} after finding the hypothesis ¬ e = b.
  • Additional details: TODO
  • ID: org.eventb.core.seqprover.shrinkEnumHypTac
  • Auto-tactic: No
  • Post-tactic: Default
  • Preference Display: Shrink Enumerated Set (Simplify)
  • Interactive: No
  • Proving Interface Display: negEnum <hypotheses names>

Before ShrinkEnumHypBefore.png

After Before ShrinkEnumHypAfter.png

Implicative Hypothesis with Conjunctive RHS

  • Description: Simplifies all (selected) hypotheses of the form P ⇒ Q ∧ R into multiple implications P ⇒ Q , P ⇒ R.
  • Additional details:
\frac{\textbf{H},\textbf{P} \limp \textbf{Q},  \textbf{P} \limp \textbf{R}\;\;\vdash \;\; \textbf{S}}{\textbf{H},\;\textbf{P} \limp  \textbf{Q} \land \textbf{R}  \;\;\vdash \;\; \textbf{S}} IMP_AND_L
  • ID: org.eventb.core.seqprover.splitRightConjImpHypTac
  • Auto-tactic: No
  • Post-tactic: Yes
  • Preference Display: Implicative Hypotheses with Conjunctive RHS (Simplify)
  • Interactive: Hypothesis

The operator is redden in the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is Implication with conjunction rewrites.

  • Proving Interface Display: ⇒ with ∧ in hyp <hypothesis name>

Before SplitRightConjImpHypBefore.png

After SplitRightConjImpHypAfter.png

Implicative Hypothesis with Disjunctive LHS

  • Description: Simplifies all (selected) hypotheses of the form P ∨ Q ⇒ R into multiple implications P ⇒ R , Q ⇒ R.
  • Additional details:
\frac{
\textbf{H},\textbf{P} \limp \textbf{R},  \textbf{Q} \limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P} \lor  \textbf{Q} \limp \textbf{R}  \;\;\vdash \;\; \textbf{S}} IMP_OR_L
  • ID: org.eventb.core.seqprover.splitLeftDisjImpHypTac
  • Auto-tactic: No
  • Post-tactic: Yes
  • Preference Display: Implicative Hypotheses with Disjunctive LHS (Simplify)
  • Interactive: Hypothesis

The operator is redden in the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is Implication with disjunction rewrites.

  • Proving Interface Display: ⇒ with ∨ in hyp <hypothesis name>

Before SplitLeftDisjImpHypBefore.png

After SplitLeftDisjImpHypAfter.png

Conjunctive Goal

  • Description: Splits a sequent with a conjunctive goal into multiple subgoals.
  • Additional details:
\frac{\textbf{H} \; \; \vdash \; \;  \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \;  \textbf{P} \; \land \; \textbf{Q}} AND_R
  • ID: org.eventb.core.seqprover.conjGoalTac
  • Auto-tactic: No
  • Post-tactic: Yes
  • Preference display: Conjunctive Goal (Split)
  • Interactive: Goal

ConjGoalInteractive.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 ConjGoalBefore.png

After ConjGoalAfter.png

Clarify Goal

  • Description: Clarifies the goal by repeatedly by:
    • splitting conjunctions,
    • simplifying implications,
    • simplifying universal quantifiers,
    • discharging sequents with a true goal, a false hypothesis and where the goal is contained in the hypotheses.
  • ID: org.eventb.core.seqprover.clarifyGoalTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference Display: Clarify Goal (Mixed)
  • Interactive: No

Functional Overriding in Goal

  • Description: TODO
  • Additional details:
\frac{\textbf{H},\; G \in \dom(g) \;\;\vdash\;\;\textbf{Q}(g(G)) \qquad \textbf{H},\; \neg\, G \in \dom(g) \;\;\vdash\;\;\textbf{Q}((\dom(g) \domsub f)(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl g)(G))} OV_R
\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F) 
\qquad \textbf{H},\; \neg\,(G=E)  \;\;\vdash\;\;\textbf{Q}((\{E\}) \domsub f)(G))}{\textbf{H} 
\;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G))} OV_SETENUM_R

where Q is WD strict.

These inference rules are applied automatically, repeatedly and recursively.

  • ID: org.eventb.core.seqprover.funOvrGoalTac
  • Auto-tactic: Default
  • Post-tactic: No
  • Preference Display: Functional Overriding in Goal (Split)
  • Interactive: Goal

When hovering the redden override operator <+, select (f<+{E|->F})(G) from the drop-down menu. (TODO strange menu item)

  • Proving Interface Display: ovr in goal

Before FunOvrGoalBefore.png

First node after application FunOvrGoalAfter1.png

Second node after application FunOvrGoalAfter2.png

Functional Overriding in Hypothesis

  • Description: TODO
  • Additional details:
\frac{\textbf{H},\; G \in \dom(g)  ,\;\textbf{P}(g(G))\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,G \in \dom(g)  ,\;\textbf{P}((\dom(g) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl g)(G)) \;\;\vdash \;\; \textbf{Q}} OV_L
\frac{\textbf{H},\; G=E  
,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(G=E)  
,\;\textbf{P}((\{E\}) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E 
\mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}} OV_SETENUM_L

where P is WD strict.

These inference rules are applied automatically, repeatedly and recursively.

  • ID: org.eventb.core.seqprover.funOvrHypTac
  • Auto-tactic: Yes
  • Post-tactic: Yes
  • Preference Display: Functional Overriding in Hypothesis (Split)
  • Interactive: Hypothesis

When hovering the redden override operator <+, select (f<+{E|->F})(G) from the drop-down menu. (TODO strange menu item)

  • Proving Interface Display: ovr in <hypothesis name>

Before FunOvrHypBefore.png

First node after application FunOvrHypAfter1.png

Second node after application FunOvrHypAfter2.png

Partition Rewriter

  • Description: Simplifies all predicates of the form partition(S, ...) into their expanded form in the goal and all visible hypotheses.
  • Additional details: TODO
  • ID: org.eventb.core.seqprover.partitionRewriteTac
  • Auto-tactic: Default
  • Post-tactic: No
  • Preference Display: Partition Rewriter (Simplify)
  • Interactive: Hypothesis, Goal

The predicate partition is redden in the goal or the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is Rewrites a partition into its definition.

  • Proving Interface Display: Partition rewrites in goal / hyp <hypothesis name>

Before PartitionRewriteBefore.png

After PartitionRewriteAfter.png

One-Point Rule in Goal

  • Description: Applies automatically the OnePointGoal tactic to the goal.
  • Additional details:
\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad  \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H}  \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} } ONE_POINT_R

The rule can be applied with ∀ as well as with ∃.

  • ID: org.eventb.core.seqprover.onePointGoalTac
  • Auto-tactic: Yes
  • Post-tactic: Yes
  • Preference Display: One Point Rule in Goal (Split)
  • Interactive: No
  • Proving Interface Display: One Point Rule in goal

Before OnePointGoalBefore.png

After OnePointGoalAfter.png

One-Point Rule in Hypothesis

  • Description: Applies automatically the OnePointHyp tactic to the selected hypotheses.
  • Additional details:
\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad  \textbf{H}, \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} \;\;\vdash \;\; \textbf{G}}{ \textbf{H}, \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R}  \;\;\vdash\;\; \textbf{G}} ONE_POINT_L

The rule can be applied with ∀ as well as with ∃.

  • ID: org.eventb.core.seqprover.onePointHypTac
  • Auto-tactic: Yes
  • Post-tactic: Yes
  • Preference Display: One Point Rule in Hypotheses (Split)
  • Interactive: No
  • Proving Interface Display: One Point Rule in hypothesis name

Before OnePointHypBefore.png

After OnePointHypAfter.png

Bounded Goal with Finite Hypothesis

  • Description: Discharges a sequent whose goal states that an expression E has a lower or a upper bound (e.g. ∃n·(∀x·x ∈ S ⇒ x ≤ n)), when there is an hypothesis that states the finiteness of E (i.e. finite(S)).
  • Additional details:
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)} FIN_L_LOWER_BOUND_L
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \geq n)} FIN_L_LOWER_BOUND_R
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \geq x)} FIN_L_UPPER_BOUND_L
\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n)} FIN_L_UPPER_BOUND_R
  • ID: org.eventb.core.seqprover.finiteHypBoundedGoalTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference Display: Bounded Goal with finite Hypothesis (Discharge)
  • Interactive: No
  • Proving Interface Display: Existence of minimum or maximum in goal with finite hypothesis

Before FiniteHypBoundedGoalBefore.png

After FiniteHypBoundedGoalAfter.png

Falsify Goal

  • Description: Contradicts the goal: the negation of the goal is taken as hypothesis and the goal becomes false.
  • Additional details:
\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \bfalse}{\textbf{H} \;\;\vdash \;\; \textbf{Q}} CONTRADICT_R


  • ID: org.eventb.ui.falsify
  • Auto-tactic: No
  • Post-tactic: No
  • Interactive: Goal
  • Proving Interface Display: ct

Before CtGoalBefore.png

After CtGoalAfter.png

Falsify Hypothesis

  • Description: Contradicts an hypothesis: the negation of the goal is taken as hypothesis and the goal becomes the negation of the contradicted hypothesis.
  • Additional details:
\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \neg\,\textbf{P}}{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}} CONTRADICT_L
  • ID: org.eventb.ui.falsify
  • Auto-tactic: No
  • Post-tactic: No
  • Interactive: Hyp
  • Proving Interface Display: ct

Before CtHypBefore.png

After CtHypAfter.png

ct has been applied to hypothesis card(S)=1.

conjI

  • Description: Splits a sequent with a conjunctive goal into multiple subgoals.
  • Additional details:
\frac{\textbf{H} \; \; \vdash \; \;  \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \;  \textbf{P} \; \land \; \textbf{Q}} AND_R
  • ID: org.eventb.core.seqprover.impI
  • Auto-tactic: No
  • Post-tactic: Yes
  • Preference Display: Conjunctive Goal (Split)
  • Interactive: No
  • Proving Interface Display: "Conjunction introduction" for manual application, "\land goal" in proof tree

Before ConjIBefore.png

After ConjIAfter.png

allI

  • Description: Simplifies any sequent with a universally quantified goal by freeing all its bound variables.
  • Additional details:
\frac{\textbf{H}\; \; \vdash \; \;  \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \;  \forall \textbf{x}\, \qdot\, \textbf{P(x)} } ALL_R
  • ID: org.eventb.core.seqprover.forallGoalTac
  • Auto-tactic: No
  • Post-tactic: Yes
  • Preference Display: For-all Goal (Simplify)
  • Interactive: Goal
  • Proving Interface Display: Forall instantiation

Before AllIBefore.png

After AllIAfter.png

exI

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ExIBefore.png

After File:ExIAfter.png

Remove Negation

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RnBefore.png

After File:RnAfter.png

Review

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ReviewBefore.png

After File:ReviewAfter.png

Proof by cases

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:DcBefore.png

After File:DcAfter.png

Add Hypothesis

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:AhBefore.png

After File:AhAfter.png

Abstract Expression

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:AeBefore.png

After File:AeAfter.png

Automatic Prover

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:AutoBefore.png

After File:AutoAfter.png

Post tactic

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:PostBefore.png

After File:PostAfter.png

Lasoo

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:LasooBefore.png

After File:LasooAfter.png

Back Tracking

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:BackBefore.png

After File:BackAfter.png

Prune

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:PruneBefore.png

After File:PruneAfter.png

Search Hypothesis

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:SearchBefore.png

After File:SearchAfter.png

Cache Hypothesis

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:CacheBefore.png

After File:CacheAfter.png

Previous

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:PreviousBefore.png

After File:PreviousAfter.png

Next

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:NextBefore.png

After File:NextAfter.png

Information

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:InformationBefore.png

After File:InformationAfter.png

Modus Ponens

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:MpBefore.png

After File:MpAfter.png

conjE

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ConjEBefore.png

After File:ConjEAfter.png

disjE

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:DisjEBefore.png

After File:DisjEAfter.png

allE

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:AllEBefore.png

After File:AllEAfter.png

exE

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ExEBefore.png

After File:ExEAfter.png


Double Implication Hypothesis

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:DblImpHypBefore.png

After File:DblImpHypAfter.png

cont Implication Hypothesis

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ContImpHypBefore.png

After File:ContImpHypAfter.png

Functional Overriding

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:FunOvrBefore.png

After File:FunOvrAfter.png


Modus Tollens

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:MtBefore.png

After File:MtAfter.png

Remove Membership

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RmBefore.png

After File:RmAfter.png

Remove Inclusion

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RiBefore.png

After File:RiAfter.png

Remove Strict-Inclusion

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RsiBefore.png

After File:RsiAfter.png

Inclusion Set Minus Right

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:IncSetMinRBefore.png

After File:IncSetMinRAfter.png

Remove Inclusion Universal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RiuBefore.png

After File:RiuAfter.png

Implication Introduction

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ImpIntBefore.png

After File:ImpIntAfter.png

Disjunction to Implication

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Disj2ImpBefore.png

After File:Disj2ImpAfter.png

Forall Modus Ponens

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:FmpBefore.png

After File:FmpAfter.png

Next Pending Sub-goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:NextPendingBefore.png

After File:NextPendingAfter.png

Next Reviewed Sub-goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:NextReviewedBefore.png

After File:NextReviewedAfter.png

impAndHyp

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ImpAndHypBefore.png

After File:ImpAndHypAfter.png

impAndGoal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ImpAndGoalBefore.png

After File:ImpAndGoalAfter.png

impOrHyp

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ImpOrHypBefore.png

After File:ImpOrHypAfter.png

impOrGoal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ImpOrGoalBefore.png

After File:ImpOrGoalAfter.png

relImgUnionRight

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RelImgUnionRightBefore.png

After File:RelImgUnionRightAfter.png

relImgUnionLeft

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RelImgUnionLeftBefore.png

After File:RelImgUnionLeftAfter.png

Set Equality

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:SetEqBefore.png

After File:SetEqAfter.png

Equivalent

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:EquivalentBefore.png

After File:EquivalentAfter.png

Functional Intersection Image

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:FunInterImgBefore.png

After File:FunInterImgAfter.png

Functional Set Minus Image

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:FunSetMinusImgBefore.png

After File:FunSetMinusImgAfter.png

Functional Singleton Image

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:FunSingImgBefore.png

After File:FunSingImgAfter.png

Converse Relation

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ConvRelBefore.png

After File:ConvRelAfter.png

Domain Distribution to the Left

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:DomDistLeftBefore.png

After File:DomDistLeftAfter.png

Domain Distribution to the Right

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:DomDistRightBefore.png

After File:DomDistRightAfter.png

Range Distribution to the Left

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RanDistLeftBefore.png

After File:RanDistLeftAfter.png

Range Distribution to the Right

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RanDistRightBefore.png

After File:RanDistRightAfter.png

Set Minus

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:SetMinusBefore.png

After File:SetMinusAfter.png

Conjunction and Disjunction Distribution

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:ConjDisjDistBefore.png

After File:ConjDisjDistAfter.png

Union Conjunction Distribution

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:UnionConjDistBefore.png

After File:UnionConjDistAfter.png

compUnionDist

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:CompUnionDistBefore.png

After File:CompUnionDistAfter.png

Domain/Range Union Distribution

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:DomRanUnionDistBefore.png

After File:DomRanUnionDistAfter.png

Relational Overriding

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RelOvrBefore.png

After File:RelOvrAfter.png

Composition Image

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:CompImgBefore.png

After File:CompImgAfter.png

Domain Composition

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:DomCompBefore.png

After File:DomCompAfter.png

Range Composition

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:RanCompBefore.png

After File:RanCompAfter.png

Functional Composition Image

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:FunCompImgBefore.png

After File:FunCompImgAfter.png

Finite Set in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Intersection in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Set Minus in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Relation in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Relation Image in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Domain in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Range in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Function in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Function Converse in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Functional Relational Image in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Functional Range in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Functional Domain in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Minimum in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Maximum in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Negative in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Finite Positive in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Cardinality Comparison in Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Cardinality Up to

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Partition Rewrite

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Arithmetic Rewrite

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png

Total Domain in Hypothesis / Goal

  • Description:
  • Additional details:
  • ID:
  • Auto-tactic:
  • Post-tactic:
  • Preference Display:
  • Interactive:
  • Proving Interface Display:

Before File:Before.png

After File:After.png