Arithmetic Rewrite Rules

From Event-B
Revision as of 15:38, 29 January 2009 by imported>Frederic (New page: {{RRHeader}} {{RRRow}}|<font size="-2"> SIMP_SPECIAL_MOD_0 </font>||<math> 0 \,\bmod\, E \;\;\defi\;\; 0 </math>|| || A {{RRRow}}|<font size="-2"> SIMP_SPECIAL_MOD_1 </font>||<math> ...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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 \mod  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   <math>i = j<math> \;\;\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   <math>i > j<math> \;\;\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 \mod  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


Some rules are not yet implemented:

  • SIMP_SPECIAL_KUNION, SIMP_SPECIAL_KUNION, SIMP_SPECIAL_KINTER, SIMP_SPECIAL_POW, SIMP_SPECIAL_POW1, SIMP_SPECIAL_CPROD_R, SIMP_SPECIAL_CPROD_L, SIMP_SPECIAL_COMPSET_BFALSE, SIMP_SPECIAL_COMPSET_BTRUE, SIMP_SPECIAL_EQUAL_COMPSET, SIMP_SPECIAL_OVERL, SIMP_SPECIAL_DOMRES_L, SIMP_SPECIAL_DOMRES_R, SIMP_SPECIAL_RANRES_R, SIMP_SPECIAL_RANRES_L, SIMP_SPECIAL_DOMSUB_L, SIMP_SPECIAL_DOMSUB_R, SIMP_SPECIAL_RANSUB_R, SIMP_SPECIAL_RANSUB_L, SIMP_SPECIAL_FCOMP, SIMP_SPECIAL_BCOMP, SIMP_SPECIAL_DPROD_R, SIMP_SPECIAL_DPROD_L, SIMP_SPECIAL_PPROD_R, SIMP_SPECIAL_PPROD_L, SIMP_SPECIAL_RELIMAGE_L, SIMP_SPECIAL_CONVERSE, SIMP_SPECIAL_ID, SIMP_SPECIAL_REL_R, SIMP_SPECIAL_REL_L, SIMP_SPECIAL_EQUAL_REL, SIMP_SPECIAL_EQUAL_RELDOM, SIMP_SPECIAL_PRJ1, SIMP_SPECIAL_PRJ2, SIMP_SPECIAL_LAMBDA, SIMP_SPECIAL_MOD_0, SIMP_SPECIAL_MOD_1, SIMP_SPECIAL_IN_NATURAL1, SIMP_SPECIAL_KBOOL_BTRUE, SIMP_SPECIAL_KBOOL_BFALSE, SIMP_SPECIAL_DIV_1, SIMP_SPECIAL_EQUAL_RELDOMRAN, SIMP_SPECIAL_FORALL_BTRUE, SIMP_SPECIAL_FORALL_BFALSE, SIMP_SPECIAL_EXIST_BTRUE, SIMP_SPECIAL_EXIST_BFALSE, SIMP_SPECIAL_SUBSET_R, SIMP_SPECIAL_SUBSET_L