Arithmetic Rewrite Rules

From Event-B
Revision as of 10:33, 8 July 2009 by imported>Laurent (Fixed rule names to make them easy to extract)
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_SETMINUS
  \card (S \setminus  T) \;\;\defi\;\;  \card (S) - \card (S \binter  T) A
*
SIMP_CARD_CPROD
  \card (S \cprod  T) \;\;\defi\;\;  \card (S) * \card (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_R
  E ^ 1 \;\;\defi\;\;  E A
*
SIMP_SPECIAL_EXPN_1_L
  1 ^ E \;\;\defi\;\;  1 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_DIV_PROD
  (X * \ldots * E * \ldots * Y) \div  E \;\;\defi\;\;  X * \ldots * Y 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