Maplet Overriding in Goal
From Event-B
Revision as of 09:44, 26 May 2011 by imported>Billaude (New page: This page describes the design of a tactic requested here : [https://sourceforge.net/tracker/index.php?func=detail&aid=3306228&group_id=108850&atid=651672 Feature Request #3306228] = Obje...)
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 :