Rodin Proof Tactics
From Event-B
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
- ID: An unique ID associated with the tactic.
- Display: Information on how an application of the tactic is displayed in the proof tree, the auto-tactic preference or the post-tactic preference.
- 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.
- Interactive: No: the tactic cannot be invoked interactively. Global: The tactic can be invoked from the Proof Control. Goal: The tactic can be invoked from the goal view. Hypothesis: The tactic can be invoked from the hypothesis view. If the tactic can be invoked interactively (i.e. either Global, Goal or Hypothesis), more information about how this could be done will be given. Note that since the Post-tactics can be launched manually, any tactics that can be included in the post-tactic in principle can be invoked interactively via the post-tactic. No here mean that there is no separate invocation for this specific tactic.
- Example: Example(s) on how the tactic can be seen from the RODIN Platform.
True Goal
- Description: Discharges any sequent whose goal is '⊤' (logical true).
- ID: org.eventb.core.seqprover.trueGoalTac
- Display: ⊤ Goal
- Auto-tactic: Default
- Post-tactic: Default
- Interactive: No
- Example: TODO
False Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Goal in Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Goal Disjunct in Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Functional Goal
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Simplification Rewriter
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Type Rewriter
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Implication Goal
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
For-all Goal
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Exists Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Find Contradictory Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Use Equality Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Shrink Implicative Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Shrink Enumerated Set
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Implicative Hypothesis with Conjunctive RHS
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Implicative Hypothesis with Disjunctive LHS
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Conjunctive Goal
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Clarify Goal
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Functional Overriding in Goal
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Functional Overriding in Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Partition Rewriter
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
One-Point Rule in Goal
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
One-Point Rule in Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO
Bounded Goal with Finite Hypothesis
- Description: TODO
- ID: TODO
- Display: TODO
- Auto-tactic: TODO
- Post-tactic: TODO
- Interactive: TODO
- Example: TODO