Arithmetic Rewrite Rules

From Event-B
Revision as of 18:16, 24 March 2009 by imported>Laurent
Jump to navigationJump to search
  Name Rule Side Condition A/M
SIMP_SPECIAL_MOD_0   0 \,\bmod\,  E \;\;\defi\;\;  0 A
SIMP_SPECIAL_MOD_1   E \,\bmod\,  1 \;\;\defi\;\;  0 A
* SIMP_MIN_SING   \min (\{ E\} ) \;\;\defi\;\;  E where E is a single expression A
* SIMP_MAX_SING   \max (\{ E\} ) \;\;\defi\;\;  E where E is a single expression A
* SIMP_MIN_NATURAL   \min (\nat ) \;\;\defi\;\;  0 A
* SIMP_MIN_NATURAL1   \min (\natn ) \;\;\defi\;\;  1 A
* SIMP_MIN_BUNION_SING   \begin{array}{cl} & \min (S \bunion  \ldots  \bunion  \{ \min (T)\}  \bunion  \ldots  \bunion  U) \\ \defi & \min (S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U) \\ \end{array} A
* SIMP_MAX_BUNION_SING   \begin{array}{cl} & \max (S \bunion  \ldots  \bunion  \{ \max (T)\}  \bunion  \ldots  \bunion  U) \\ \defi &  \max (S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U) \\  \end{array} A
* SIMP_MIN_UPTO   \min (E \upto  F) \;\;\defi\;\;  E A
* SIMP_MAX_UPTO   \max (E \upto  F) \;\;\defi\;\;  F A
* SIMP_LIT_MIN   \min (\{ E, \ldots  , i, \ldots  , j, \ldots , H\} ) \;\;\defi\;\;  \min (\{ E, \ldots  , i, \ldots , H\} ) where i and j are literals and i \leq j A
* SIMP_LIT_MAX   \max (\{ E, \ldots  , i, \ldots  , j, \ldots , H\} ) \;\;\defi\;\;  \max (\{ E, \ldots  , i, \ldots , H\} ) where i and j are literals and i \geq j A
* SIMP_LIT_MIN_UPTO   \min (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) where i, ... ,\,j are literals A
* SIMP_LIT_MAX_UPTO   \max (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) where i, ... ,\,j are literals A
* SIMP_SPECIAL_CARD   \card (\emptyset ) \;\;\defi\;\;  0 A
* SIMP_CARD_SING   \card (\{ E\} ) \;\;\defi\;\;  1 where E is a single expression A
* SIMP_SPECIAL_EQUAL_CARD   \card (S) = 0 \;\;\defi\;\;  S = \emptyset A
* SIMP_CARD_POW   \card (\pow (S)) \;\;\defi\;\;  2 ^ \card (S) A
* SIMP_CARD_BUNION   \card (S \bunion  T) \;\;\defi\;\;  \card (S) + \card (T) - \card (S \binter  T) A
* SIMP_CARD_CONVERSE   \card (r^{-1} ) \;\;\defi\;\;  \card (r) A
* SIMP_CARD_ID   \card (\id (S)) \;\;\defi\;\;  \card (S) A
* SIMP_CARD_LAMBDA   \card (\lambda x\qdot (P \mid  E)) \;\;\defi\;\;  \card (\{ x \qdot  P \mid  x\} ) A
* SIMP_CARD_COMPSET   \card (\{ x \qdot  x \in  S \mid  x\} ) \;\;\defi\;\;  \card (S) where x non free in S A
* SIMP_LIT_CARD_UPTO   \card (i \upto  j) \;\;\defi\;\;  j-i+1 where i and j are literals and i \leq j A
* SIMP_TYPE_CARD   \card (\mathit{Tenum}) \;\;\defi\;\;  N where \mathit{Tenum} is a carrier set containing N elements A
* SIMP_LIT_GE_CARD_0   \card (S) \geq  1 \;\;\defi\;\;  \lnot\, S = \emptyset A
* SIMP_LIT_LE_CARD_1   1 \leq  \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset A
* SIMP_LIT_LE_CARD_0   0 \leq  \card (S) \;\;\defi\;\;  \btrue A
* SIMP_LIT_GE_CARD_0   \card (S) \geq  0 \;\;\defi\;\;  \btrue A
* SIMP_LIT_GT_CARD_0   \card (S) > 0 \;\;\defi\;\;  \lnot\, S = \emptyset A
* SIMP_LIT_LT_CARD_0   0 < \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset A
* SIMP_LIT_EQUAL_CARD_1   \card (S) = 1 \;\;\defi\;\;  \exists x \qdot  S = \{ x\} A
* SIMP_CARD_NATURAL   \card (S) \in  \nat  \;\;\defi\;\;  \btrue A
* SIMP_CARD_NATURAL1   \card (S) \in  \natn  \;\;\defi\;\;  \lnot\, S = \emptyset A
* SIMP_LIT_IN_NATURAL   i \in  \nat  \;\;\defi\;\;  \btrue where i is a literal A
SIMP_SPECIAL_IN_NATURAL1   0 \in  \natn  \;\;\defi\;\;  \bfalse A
* SIMP_LIT_IN_NATURAL1   i \in  \natn  \;\;\defi\;\;  \btrue where i is a literal and 1 \leq i A
* SIMP_LIT_UPTO   i \upto  j \;\;\defi\;\;  \emptyset where i and j are literals and j < i A
* SIMP_LIT_IN_MINUS_NATURAL   -i \in  \nat  \;\;\defi\;\;  \bfalse where i is a literal and 1 \leq i A
* SIMP_LIT_IN_MINUS_NATURAL1   -i \in  \natn  \;\;\defi\;\;  \bfalse where i is a literal A
SIMP_SPECIAL_KBOOL_BTRUE   \bool (\btrue ) \;\;\defi\;\;  \True A
SIMP_SPECIAL_KBOOL_BFALSE   \bool (\bfalse ) \;\;\defi\;\;  \False A
* SIMP_LIT_EQUAL_KBOOL_TRUE   \bool (P) = \True  \;\;\defi\;\;  P A
* SIMP_LIT_EQUAL_KBOOL_FALSE   \bool (P) = \False  \;\;\defi\;\;  \lnot\, P A
* DEF_EQUAL_MIN   E = \min (S) \;\;\defi\;\;  E \in  S \land  (\forall x \qdot  x \in  S \limp  E \leq  x) where x non free in S, E M
* DEF_EQUAL_MAX   E = \max (S) \;\;\defi\;\;  E \in  S \land  (\forall x \qdot  x \in  S \limp  E \geq  x) where x non free in S, E M
* SIMP_SPECIAL_PLUS   E + \ldots  + 0 + \ldots  + F \;\;\defi\;\;  E + \ldots  + F A
* SIMP_SPECIAL_MINUS_R   E - 0 \;\;\defi\;\;  E A
* SIMP_SPECIAL_MINUS_L   0 - E \;\;\defi\;\;  -E A
* SIMP_MINUS_MINUS    - (- E) \;\;\defi\;\;  E A
* SIMP_MULTI_MINUS   E - E \;\;\defi\;\;  0 A
* SIMP_SPECIAL_PROD_0   E * \ldots  * 0 * \ldots  * F \;\;\defi\;\;  0 A
* SIMP_SPECIAL_PROD_1   E * \ldots  * 1 * \ldots  * F \;\;\defi\;\;  E * \ldots  * F A
* SIMP_SPECIAL_PROD_MINUS_EVEN   (-E) * \ldots  * (-F) \;\;\defi\;\;  E * \ldots  * F if an even number of - A
* SIMP_SPECIAL_PROD_MINUS_ODD   (-E) * \ldots  * (-F) \;\;\defi\;\;  -(E * \ldots  * F) if an odd number of - A
* SIMP_LIT_MINUS    - (i) \;\;\defi\;\;  (-i) where i is a literal A
* SIMP_LIT_MINUS_MINUS    - (-i) \;\;\defi\;\;  i where i is a literal A
* SIMP_LIT_EQUAL   i = j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) where i and j are literals A
* SIMP_LIT_LE   i \leq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) where i and j are literals A
* SIMP_LIT_LT   i < j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) where i and j are literals A
* SIMP_LIT_GE   i \geq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) where i and j are literals A
* SIMP_LIT_GT   i > j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) where i and j are literals A
* SIMP_DIV_MINUS   (- E) \div  (-F) \;\;\defi\;\;  E \div  F A
SIMP_SPECIAL_DIV_1   E \div  1 \;\;\defi\;\;  E A
* SIMP_SPECIAL_DIV_0   0 \div  E \;\;\defi\;\;  0 A
* SIMP_SPECIAL_EXPN_1   E ^ 1 \;\;\defi\;\;  E A
* SIMP_SPECIAL_EXPN_0   E ^ 0 \;\;\defi\;\;  1 A
* SIMP_MULTI_LE   E \leq  E \;\;\defi\;\;  \btrue A
* SIMP_MULTI_LT   E < E \;\;\defi\;\;  \bfalse A
* SIMP_MULTI_GE   E \geq  E \;\;\defi\;\;  \btrue A
* SIMP_MULTI_GT   E > E \;\;\defi\;\;  \bfalse A
* SIMP_MULTI_DIV   E \div  E \;\;\defi\;\;  1 A
* SIMP_MULTI_MOD   E \,\bmod\,  E \;\;\defi\;\;  0 A
* DISTRI_PROD_PLUS   a * (b + c) \;\;\defi\;\;  (a * b) + (a * c) M
* DISTRI_PROD_MINUS   a * (b - c) \;\;\defi\;\;  (a * b) - (a * c) M
* DERIV_LE_CARD   \card (S) \leq  \card (T) \;\;\defi\;\;  S \subseteq  T S and T must be of the same type M
* DERIV_GE_CARD   \card (S) \geq  \card (T) \;\;\defi\;\;  T \subseteq  S S and T must be of the same type M
* DERIV_LT_CARD   \card (S) < \card (T) \;\;\defi\;\;  S  \subset  T S and T must be of the same type M
* DERIV_GT_CARD   \card (S) > \card (T) \;\;\defi\;\;  T  \subset  S S and T must be of the same type M
* DERIV_EQUAL_CARD   \card (S) = \card (T) \;\;\defi\;\;  S = T  S and T must be of the same type M