Maplet Overriding in Goal: Difference between revisions
From Event-B
Jump to navigationJump to search
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... |
imported>Billaude |
||
Line 3: | Line 3: | ||
= Objective = | = Objective = | ||
Split every goal in the form : <math> f \ovl{ | Split every goal in the form : <math> f \ovl{\{x \mapsto y\}} \in A \to B </math> into three sub-goals : | ||
:*<math>{x} \domsub f \in A \smallsetminus | :*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to B</math> | ||
:*<math>x \in A</math> | :*<math>x \in A</math> | ||
:*<math>y \in B</math> | :*<math>y \in B</math> |
Revision as of 13:08, 30 May 2011
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 :