Difference between pages "Main Page" and "Maplet Overriding in Goal"
From Event-B
(Difference between pages)
Jump to navigationJump to searchimported>WikiSysop |
imported>Billaude |
||
Line 1: | Line 1: | ||
− | == | + | 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] |
− | + | = Objective = | |
− | + | 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 \{x\} \to B</math> | ||
+ | :*<math>x \in A</math> | ||
+ | :*<math>y \in B</math> | ||
− | + | = Design Decision = | |
− | + | Instead of proofing the first sub-goal, it may be more easy to proof <math>f\in A\to B</math> which is a sufficient condition : <math>(f\in A\to B)\limp (\{x\} \domsub f \in A \smallsetminus \{x\} \to B)</math>. | |
− | [[ | + | = Implementation = |
+ | |||
+ | First, the goal is checked. Its tree structure must match the following one : | ||
+ | <math>\in</math> | ||
+ | ├── <math>\ovl</math> | ||
+ | │ ├── f | ||
+ | │ └── {} | ||
+ | │ └── <math>\mapsto</math> | ||
+ | │ ├── x | ||
+ | │ └── y | ||
+ | └── <math>\to</math> | ||
+ | ├── A | ||
+ | └── B | ||
+ | Then, if the hypothesis <math>f\in A\to B</math> is contained in the hypothesis the goal is splitted as follows : | ||
+ | :*<math>f\in A\to B</math> | ||
+ | :*<math>x \in A</math> | ||
+ | :*<math>y \in B</math> | ||
+ | Else, it is splitted as follows : | ||
+ | :*<math>{x} \domsub f \in A \smallsetminus \left\{x\right\} \to B</math> | ||
+ | :*<math>x \in A</math> | ||
+ | :*<math>y \in B</math> | ||
+ | |||
+ | [[Category:Design proposal]] |
Revision as of 13:09, 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 :