# Changes to the Mathematical Language of Event-B

This document describes the evolution of the Event-B mathematical language that happened in release 1.0.0. See Event-B_Mathematical_Language for a full description of the language.

## Contents

## Generic Identity and Projections

Three operators were still unary while they could be atomic and generic:

- the identity relation <math>\id</math>
- the first projection <math>\prjone</math>
- the second projection <math>\prjtwo</math>

These operators are defined as follows in the old version:

<math> \begin{matrix} E\mapsto F &\in\id(S) && E\in S\;\land\; F = E\\ (E\mapsto F)\mapsto G &\in\prjone(r) && E\mapsto F\in r\;\land\; G = E\\ (E\mapsto F)\mapsto G &\in\prjtwo(r) && E\mapsto F\in r\;\land\; G = F . \end{matrix} </math>

If we drop the parameter, we get much more straightforward definitions that capture the essence of the operator. The new definitions are

<math> \begin{matrix} E\mapsto F &\in\id && E = F\\ (E\mapsto F)\mapsto G &\in\prjone && E = G\\ (E\mapsto F)\mapsto G &\in\prjtwo && F = G . \end{matrix} </math>

We have the following equivalence between the old and the new versions of the operators

<math> \begin{matrix} \textbf{Old Version} & \textbf{New Version}\\ \id(S) & S\domres id\\ \prjone(r) & r\domres\prjone\\ \prjtwo(r) & r\domres\prjtwo . \end{matrix} </math>

Moreover, in the case where the parameter is not needed, then it can be dropped altogether: no domain restriction is needed. For instance, to express that a relation <math>r</math> is irreflexive, one would now write <math>r\binter\id = \emptyset</math>.

## Partition

A new partition predicate is introduced. It is intended to provide an easier way to enter enumerated sets, while getting rid of the <math>\frac{n(n-1)}{2}</math> axioms needed to express pairwise distinctness (or disjointness). The partition operator is defined as follows:

<math> \begin{array}{ll} partition(E_0, E_1, \ldots, E_n)\defi & E_0 = E_1\bunion \cdots\bunion E_n \\ & \;\land\; E_1\binter E_2=\emptyset \;\land\;\cdots \;\land\; E_{n-1}\binter E_n = \emptyset \\ & (\;\land\; i \ne j \limp E_i \binter E_j = \emptyset ) \\ \end{array} </math>

where the <math>E_i</math> are expressions bearing the same type.

Then, we can enter into a context :

<math> \begin{array}{ll} \mathsf{set} & S\\ \mathsf{constant} & a_1\\ \vdots & \vdots\\ \mathsf{constant} & a_n\\ \mathsf{axiom} & partition(S, \{a_1\}, \ldots, \{a_n\}) \end{array} </math>

which is a particular case of a set being defined by listing all its elements.

### Partition Wizard

**TODO**

## Operator Associativity

Operators used to build sets of relations or functions, viz.

- relation
- total relation
- surjective relation
- total surjective relation
- partial function
- total function
- partial injection
- total injection
- partial surjection
- total surjection
- bijection

have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.