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...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

This page describes the design of a tactic requested here : Feature Request #3306228

Objective

Split every goal in the form :  f \ovl{\left\{x \mapsto y\right\}} \in A \to B into three sub-goals :

  • {x} \domsub f \in A \smallsetminus \left\{x\right\} \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 \left\{x\right\} \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