Maplet Overriding in Goal
From Event-B
This page describes the design of a tactic requested here : Feature Request #3306228
Objective
Split every goal in the form : into three sub-goals :
Design Decision
Instead of proofing the first sub-goal, it may be more easy to proof which is a sufficient condition : .
Implementation
First, the goal is checked. Its tree structure must match the following one :
├── │ ├── f │ └── {} │ └── │ ├── x │ └── y └── ├── A └── B
Then, if the hypothesis is contained in the hypothesis the goal is splitted as follows :
Else, it is splitted as follows :