Rodin User’s Handbook v.2.8: Substitutions

Rodin Handbook

This work is sponsored by the Deploy Project

This work is sponsored by the ADVANCE Project

Creative Commons License

Creative Commons License

This work is licensed under a Creative Commons Attribution 3.0 Unported License

Substitutions

Rodin User’s Handbook v.2.8

3.2.2 Substitutions

We use the notation $P[E/x]$ for a substitution of all free occurrences of the variable $x$ in $P$ by the expression $E$ . Several substitutions can be performed simultaneously with $P(E_1/x_1,\ldots ,E_ n/x_ n)$ . In particular, we use the syntax $P[\mathbf{x}’/\mathbf{x}]$ to denote the substitution of each identifier $x$ in the sequence $\mathbf{x}$ by $x’$ . For more information on free identifiers, see Section 3.3.1.3.

Examples:

$(x>y)[5+2/y]$ corresponds to the predicate $(x>5+2)$ .
$(x>y)[2\cdot y/x,5+2/y]$ corresponds to the predicate $(2\cdot y>5+2)$ .
$(\exists x \mathord {\mkern 1mu\cdot \mkern 1mu}x\in S \land x>y)[2\cdot y/x,5+2/y]$ corresponds to the predicate $(\exists x \mathord {\mkern 1mu\cdot \mkern 1mu}x\in S \land x>5+2)$ , because the $x$ is a quantified variable (i.e. it is not a free variable).
For a sequence $\mathbf{v}=v_1,v_2,v_3$ the predicate $(v_1\subseteq v_2\land v_3\in v_1)[\mathbf{v}’/\mathbf{v}]$ corresponds to $(v_1’\subseteq v_2’\land v_3’\in v_1’)$ .

Rodin User’s Handbook v.2.8 : Reference : Event-B’s modelling notation : Substitutions