Difference between pages "Main Page" and "Maplet Overriding in Goal"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>WikiSysop
 
imported>Billaude
 
Line 1: Line 1:
== Event-B and Rodin Documentation Wiki ==
+
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]
  
[[Event-B Language]]
+
= Objective =
  
[[Rodin Platform|Rodin Platform User Support]]
+
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>
  
[[Rodin Plug-ins|Rodin Plug-in User Support]]
+
= Design Decision =
  
[[Rodin Developer Support]]
+
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>.
  
[[Test area]]
+
= 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 :  f \ovl{\{x \mapsto y\}} \in A \to B into three sub-goals :

  • \{x\} \domsub f \in A \smallsetminus \{x\} \to B
  • x \in A
  • y \in B

Design Decision

Instead of proofing the first sub-goal, it may be more easy to proof f\in A\to B which is a sufficient condition : (f\in A\to B)\limp (\{x\} \domsub f \in A \smallsetminus \{x\} \to B).

Implementation

First, the goal is checked. Its tree structure must match the following one :

\in
├── \ovl
│   ├── f
│   └── {}
│       └──  \mapsto
│            ├── x
│            └── y
└── \to
    ├── A
    └── B

Then, if the hypothesis f\in A\to B is contained in the hypothesis the goal is splitted as follows :

  • f\in A\to B
  • x \in A
  • y \in B

Else, it is splitted as follows :

  • {x} \domsub f \in A \smallsetminus \left\{x\right\} \to B
  • x \in A
  • y \in B