View source for Rewriting rules for event model decomposition

The purpose of this page is to list and justify the rewriting / simplification rules applied in the event model decomposition when building the ''external'' events, and more especially their actions.

== Rewriting rules for the Event-B assignments ==
As detailed in [[Actions_(Modelling_Language)|the modelling language]], the Event-B assignments are formed of two parts: 
* a left-hand side, which is a list of free identifiers.
* a right-hand side.

There are various kinds of assignments:
* The <math>\bcmsuch</math> ("becomes such that") assignment is the most general (non-deterministic) assignment, where a predicate is given on the before and after values of assigned identifiers. The after values of the assigned identifiers are denoted by a primed identifier whose prefix is the assigned identifier. 
* The <math>\bcmeq</math> ("becomes equal to") assignment is the deterministic assignment where an expression is given for each assigned identifier.
* The <math>\bcmin</math> ("becomes member of") assignment is the set-based (non-deterministic) assignment, where a set expression is given for the assigned identifier.

Let <math>v</math> and <math>w</math> be variables, and <math>E</math> and <math>F</math> be expressions. In the following table, the left-hand assignments are equivalent (<math>\defi</math>) to the right-hand ones:
{{SimpleHeader}}
|-
|<math>v \bcmeq E</math>||<math>v \bcmsuch v' = E</math>
|-
|<math>v,w \bcmeq E,F</math>||<math>v \bcmeq E \pprod w \bcmeq F</math>
|-
|<math>v(E) \bcmeq F</math>||<math>v \bcmeq v \ovl \{E \mapsto F\}</math>
|-
|<math>v \bcmin E</math>||<math>v \bcmsuch v' \in E</math>
|}

Thus, each Event-B assignment can be expressed in a "becomes such that" form.

== Simplification rules on Event-B predicates ==

== Rewriting rules for the Event-B actions ==
Let <math>v</math> and <math>w</math> be variables, and  <math>P</math> and <math>Q</math> be predicates. The following equivalence applies :

{|
|<math>v~ \bcmsuch P(v,v')</math><br><math>w \bcmsuch Q(w,w')</math>||&nbsp;&nbsp;&nbsp;&nbsp;<math>\defi\;\; v,w \bcmsuch P(v,v') \land Q(w,w')</math>
|}

== Simplification rules based on Event-B proof obligations ==