Adding Manual Rewrite Reasoners

Manual rewrite Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses. Hence beside the input sequent, reasoners of this type have an extra input to specify the location of the (sub-)formula where the rewriting should carry out. We take the example of which rewrites according to the following rules for implication.

$\begin{array}{rcl} \top \limp P & \Rightarrow & P \\ P \limp \top & \Rightarrow & \top \\ \bot \limp P & \Rightarrow & \top \\ P \limp \bot & \Rightarrow & \neg P \end{array}$

We can reuse some of the code that we already developed for the automatic rewrite reasoner.

Below are the step by step instructions to create an automatic rewrite reasoner:

Create the Reasoner

• Create a new plug-in project, e.g. org.eventb.contributors.seqprover.implrewrites. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI".

• Add dependency on the project org.eventb.core.seqprover

• Add an extension for org.eventb.core.seqprover.reasoners for our implication rewrite reasoner, e.g.

<extension point="org.eventb.core.seqprover.reasoners">
  <reasoner
    class="org.eventb.internal.contributors.seqprover.implrewrites.ManualReasoner"
    id="manualReasoner"
    name="%manualReasonerName"/>
</extension>

(add the key manualReasonerName to the plugin.properties accordingly).