Arithmetic Rewrite Rules

From Event-B
Jump to: navigation, search

Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.


  Name Rule Side Condition A/M
*
SIMP_SPECIAL_MOD_0
<math> 0 \,\bmod\, E \;\;\defi\;\; 0 </math> A
*
SIMP_SPECIAL_MOD_1
<math> E \,\bmod\, 1 \;\;\defi\;\; 0 </math> A
*
SIMP_MIN_SING
<math> \min (\{ E\} ) \;\;\defi\;\; E </math> where <math>E</math> is a single expression A
*
SIMP_MAX_SING
<math> \max (\{ E\} ) \;\;\defi\;\; E </math> where <math>E</math> is a single expression A
*
SIMP_MIN_NATURAL
<math> \min (\nat ) \;\;\defi\;\; 0 </math> A
*
SIMP_MIN_NATURAL1
<math> \min (\natn ) \;\;\defi\;\; 1 </math> A
*
SIMP_MIN_BUNION_SING
<math> \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} </math> A
*
SIMP_MAX_BUNION_SING
<math> \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} </math> A
*
SIMP_MIN_UPTO
<math> \min (E \upto F) \;\;\defi\;\; E </math> A
*
SIMP_MAX_UPTO
<math> \max (E \upto F) \;\;\defi\;\; F </math> A
*
SIMP_LIT_MIN
<math> \min (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \min (\{ E, \ldots , i, \ldots , H\} ) </math> where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> A
*
SIMP_LIT_MAX
<math> \max (\{ E, \ldots , i, \ldots , j, \ldots , H\} ) \;\;\defi\;\; \max (\{ E, \ldots , i, \ldots , H\} ) </math> where <math>i</math> and <math>j</math> are literals and <math>i \geq j</math> A
*
SIMP_SPECIAL_CARD
<math> \card (\emptyset ) \;\;\defi\;\; 0 </math> A
*
SIMP_CARD_SING
<math> \card (\{ E\} ) \;\;\defi\;\; 1 </math> where <math>E</math> is a single expression A
*
SIMP_SPECIAL_EQUAL_CARD
<math> \card (S) = 0 \;\;\defi\;\; S = \emptyset </math> A
*
SIMP_CARD_POW
<math> \card (\pow (S)) \;\;\defi\;\; 2\expn{\card(S)} </math> A
*
SIMP_CARD_BUNION
<math> \card (S \bunion T) \;\;\defi\;\; \card (S) + \card (T) - \card (S \binter T) </math> A
SIMP_CARD_SETMINUS
<math>\card(S\setminus T)\;\;\defi\;\;\card(S) - \card(T)</math> with hypotheses <math>T\subseteq S</math> and either <math>\finite(S)</math> or <math>\finite(T)</math> A
SIMP_CARD_SETMINUS_SETENUM
<math>\card(S\setminus\{E_1,\ldots,E_n\})\;\;\defi\;\;\card(S) - \card(\{E_1,\ldots,E_n\})</math> with hypotheses <math>E_i\in S</math> for all <math>i\in 1\upto n</math> A
*
SIMP_CARD_CONVERSE
<math> \card (r^{-1} ) \;\;\defi\;\; \card (r) </math> A
*
SIMP_CARD_ID
<math> \card (\id) \;\;\defi\;\; \card (S) </math> where <math>\id</math> has type <math>\pow (S \cprod S) </math> A
*
SIMP_CARD_ID_DOMRES
<math> \card (S\domres\id) \;\;\defi\;\; \card (S) </math> A
*
SIMP_CARD_PRJ1
<math> \card (\prjone) \;\;\defi\;\; \card (S \cprod T) </math> where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> A
*
SIMP_CARD_PRJ2
<math> \card (\prjtwo) \;\;\defi\;\; \card (S \cprod T) </math> where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> A
*
SIMP_CARD_PRJ1_DOMRES
<math> \card (E \domres \prjone) \;\;\defi\;\; \card (E) </math> A
*
SIMP_CARD_PRJ2_DOMRES
<math> \card (E \domres \prjtwo) \;\;\defi\;\; \card (E) </math> A
*
SIMP_CARD_LAMBDA
<math> \card(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \card(\{x\qdot P\mid E\} ) </math> where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> A
*
SIMP_LIT_CARD_UPTO
<math> \card (i \upto j) \;\;\defi\;\; j-i+1 </math> where <math>i</math> and <math>j</math> are literals and <math>i \leq j</math> A
SIMP_TYPE_CARD
<math> \card (\mathit{Tenum}) \;\;\defi\;\; N </math> where <math>\mathit{Tenum}</math> is a carrier set containing <math>N</math> elements A
*
SIMP_LIT_GE_CARD_1
<math> \card (S) \geq 1 \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_LE_CARD_1
<math> 1 \leq \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_LE_CARD_0
<math> 0 \leq \card (S) \;\;\defi\;\; \btrue </math> A
*
SIMP_LIT_GE_CARD_0
<math> \card (S) \geq 0 \;\;\defi\;\; \btrue </math> A
*
SIMP_LIT_GT_CARD_0
<math> \card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_LT_CARD_0
<math> 0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_EQUAL_CARD_1
<math> \card (S) = 1 \;\;\defi\;\; \exists x \qdot S = \{ x\} </math> A
*
SIMP_CARD_NATURAL
<math> \card (S) \in \nat \;\;\defi\;\; \btrue </math> A
*
SIMP_CARD_NATURAL1
<math> \card (S) \in \natn \;\;\defi\;\; \lnot\, S = \emptyset </math> A
*
SIMP_LIT_IN_NATURAL
<math> i \in \nat \;\;\defi\;\; \btrue </math> where <math>i</math> is a non-negative literal A
*
SIMP_SPECIAL_IN_NATURAL1
<math> 0 \in \natn \;\;\defi\;\; \bfalse </math> A
*
SIMP_LIT_IN_NATURAL1
<math> i \in \natn \;\;\defi\;\; \btrue </math> where <math>i</math> is a positive literal A
*
SIMP_LIT_UPTO
<math> i \upto j \;\;\defi\;\; \emptyset </math> where <math>i</math> and <math>j</math> are literals and <math>j < i</math> A
*
SIMP_LIT_IN_MINUS_NATURAL
<math> -i \in \nat \;\;\defi\;\; \bfalse </math> where <math>i</math> is a positive literal A
*
SIMP_LIT_IN_MINUS_NATURAL1
<math> -i \in \natn \;\;\defi\;\; \bfalse </math> where <math>i</math> is a non-negative literal A
*
DEF_IN_NATURAL
<math>x \in \nat \;\;\defi\;\; 0 \leq x </math> M
*
DEF_IN_NATURAL1
<math>x \in \natn \;\;\defi\;\; 1 \leq x </math> M
*
SIMP_LIT_EQUAL_KBOOL_TRUE
<math> \bool (P) = \True \;\;\defi\;\; P </math> A
*
SIMP_LIT_EQUAL_KBOOL_FALSE
<math> \bool (P) = \False \;\;\defi\;\; \lnot\, P </math> A
DEF_EQUAL_MIN
<math> E = \min (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \leq x) </math> where <math>x</math> non free in <math>S, E</math> M
DEF_EQUAL_MAX
<math> E = \max (S) \;\;\defi\;\; E \in S \land (\forall x \qdot x \in S \limp E \geq x) </math> where <math>x</math> non free in <math>S, E</math> M
*
SIMP_SPECIAL_PLUS
<math> E + \ldots + 0 + \ldots + F \;\;\defi\;\; E + \ldots + F </math> A
*
SIMP_SPECIAL_MINUS_R
<math> E - 0 \;\;\defi\;\; E </math> A
*
SIMP_SPECIAL_MINUS_L
<math> 0 - E \;\;\defi\;\; -E </math> A
*
SIMP_MINUS_MINUS
<math> - (- E) \;\;\defi\;\; E </math> A
*
SIMP_MINUS_UNMINUS
<math> E - (- F) \;\;\defi\;\; E + F </math> where <math>(-F)</math> is a unary minus expression or a negative literal M
*
SIMP_MULTI_MINUS
<math> E - E \;\;\defi\;\; 0 </math> A
*
SIMP_MULTI_MINUS_PLUS_L
<math> (A + \ldots + C + \ldots + B) - C \;\;\defi\;\; A + \ldots + B </math> M
*
SIMP_MULTI_MINUS_PLUS_R
<math> C - (A + \ldots + C + \ldots + B) \;\;\defi\;\; -(A + \ldots + B) </math> M
*
SIMP_MULTI_MINUS_PLUS_PLUS
<math> (A + \ldots + E + \ldots + B) - (C + \ldots + E + \ldots + D) \;\;\defi\;\; (A + \ldots + B) - (C + \ldots + D) </math> M
*
SIMP_MULTI_PLUS_MINUS
<math>(A + \ldots + D + \ldots + (C - D) + \ldots + B) \;\;\defi\;\; A + \ldots + C + \ldots + B </math> M
*
SIMP_MULTI_ARITHREL_PLUS_PLUS
<math> A + \ldots + E + \ldots + B < C + \ldots + E + \ldots + D \;\;\defi\;\; A + \ldots + B < C + \ldots + D </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_PLUS_R
<math> C < A + \ldots + C \ldots + B \;\;\defi\;\; 0 < A + \ldots + B </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_PLUS_L
<math> A + \ldots + C \ldots + B < C \;\;\defi\;\; A + \ldots + B < 0 </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_R
<math> A - C < B - C \;\;\defi\;\; A < B </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_L
<math> C - A < C - B \;\;\defi\;\; B < A </math> where the root relation (<math><</math> here) is one of <math>\{=, <, \leq, >, \geq\}</math> M
*
SIMP_SPECIAL_PROD_0
<math> E * \ldots * 0 * \ldots * F \;\;\defi\;\; 0 </math> A
*
SIMP_SPECIAL_PROD_1
<math> E * \ldots * 1 * \ldots * F \;\;\defi\;\; E * \ldots * F </math> A
*
SIMP_SPECIAL_PROD_MINUS_EVEN
<math> (-E) * \ldots * (-F) \;\;\defi\;\; E * \ldots * F </math> if an even number of <math>-</math> A
*
SIMP_SPECIAL_PROD_MINUS_ODD
<math> (-E) * \ldots * (-F) \;\;\defi\;\; -(E * \ldots * F) </math> if an odd number of <math>-</math> A
*
SIMP_LIT_MINUS
<math> - (i) \;\;\defi\;\; (-i) </math> where <math>i</math> is a literal A
*
SIMP_LIT_EQUAL
<math> i = j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_LE
<math> i \leq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_LT
<math> i < j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_GE
<math> i \geq j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_LIT_GT
<math> i > j \;\;\defi\;\; \btrue \;or\; \bfalse \;\;(computation) </math> where <math>i</math> and <math>j</math> are literals A
*
SIMP_DIV_MINUS
<math> (- E) \div (-F) \;\;\defi\;\; E \div F </math> A
*
SIMP_SPECIAL_DIV_1
<math> E \div 1 \;\;\defi\;\; E </math> A
*
SIMP_SPECIAL_DIV_0
<math> 0 \div E \;\;\defi\;\; 0 </math> A
*
SIMP_SPECIAL_EXPN_1_R
<math> E ^ 1 \;\;\defi\;\; E </math> A
*
SIMP_SPECIAL_EXPN_1_L
<math> 1 ^ E \;\;\defi\;\; 1 </math> A
*
SIMP_SPECIAL_EXPN_0
<math> E ^ 0 \;\;\defi\;\; 1 </math> A
*
SIMP_MULTI_LE
<math> E \leq E \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_LT
<math> E < E \;\;\defi\;\; \bfalse </math> A
*
SIMP_MULTI_GE
<math> E \geq E \;\;\defi\;\; \btrue </math> A
*
SIMP_MULTI_GT
<math> E > E \;\;\defi\;\; \bfalse </math> A
*
SIMP_MULTI_DIV
<math> E \div E \;\;\defi\;\; 1 </math> A
*
SIMP_MULTI_DIV_PROD
<math> (X * \ldots * E * \ldots * Y) \div E \;\;\defi\;\; X * \ldots * Y </math> A
*
SIMP_MULTI_MOD
<math> E \,\bmod\, E \;\;\defi\;\; 0 </math> A
DISTRI_PROD_PLUS
<math> a * (b + c) \;\;\defi\;\; (a * b) + (a * c) </math> M
DISTRI_PROD_MINUS
<math> a * (b - c) \;\;\defi\;\; (a * b) - (a * c) </math> M
DERIV_NOT_EQUAL
<math> \lnot E = F \;\;\defi\;\; E < F \lor E > F </math> <math>E</math> and <math>F</math> must be of Integer type M