Arithmetic Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Laurent
m Fixed rule names to make them easy to extract
Guillaume (talk | contribs)
53 edits
Rules DEF_EXPN_STEP, SIMP_{MIN,MAX}_IN and SIMP_KBOOL_LIT_EQUAL_TRUE have been implemented in Rodin 3.9
 
(34 intermediate revisions by 6 users not shown)
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
Rules without a <tt>*</tt> are planned to be implemented in future versions.
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
{{RRHeader}}
{{RRHeader}}
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_MOD_0}}||<math>  0 \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MOD_0}}||<math>  0 \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_MOD_1}}||<math>  E \,\bmod\,  1 \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MOD_1}}||<math>  E \,\bmod\,  1 \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_SING}}||<math>  \min (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_SING}}||<math>  \min (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_SING}}||<math>  \max (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_SING}}||<math>  \max (\{ E\} ) \;\;\defi\;\;  E </math>|| where <math>E</math> is a single expression ||  A
Line 10: Line 14:
{{RRRow}}|*||{{Rulename|SIMP_MIN_UPTO}}||<math>  \min (E \upto  F) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_UPTO}}||<math>  \min (E \upto  F) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_UPTO}}||<math>  \max (E \upto  F) \;\;\defi\;\;  F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_UPTO}}||<math>  \max (E \upto  F) \;\;\defi\;\;  F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MIN_IN}}||<math>  \min (S) \in S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MAX_IN}}||<math>  \max (S) \in S \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_LIT_MIN_UPTO}}||<math>  \min (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MAX_UPTO}}||<math>  \max (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CARD}}||<math>  \card (\emptyset ) \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CARD}}||<math>  \card (\emptyset ) \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_SING}}||<math>  \card (\{ E\} ) \;\;\defi\;\;  1 </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_SING}}||<math>  \card (\{ E\} ) \;\;\defi\;\;  1 </math>|| where <math>E</math> is a single expression ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_CARD}}||<math>  \card (S) = 0 \;\;\defi\;\;  S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_CARD}}||<math>  \card (S) = 0 \;\;\defi\;\;  S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_POW}}||<math>  \card (\pow (S)) \;\;\defi\;\;  2 ^ \card (S) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_POW}}||<math>  \card (\pow (S)) \;\;\defi\;\;  2\expn{\card(S)} </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_BUNION}}||<math>  \card (S \bunion  T) \;\;\defi\;\;  \card (S) + \card (T) - \card (S \binter  T) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_BUNION}}||<math>  \card (S \bunion  T) \;\;\defi\;\;  \card (S) + \card (T) - \card (S \binter  T) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_SETMINUS}}||<math> \card (S \setminus T) \;\;\defi\;\; \card (S) - \card (S \binter  T) </math>||  ||  A
{{RRRow}}| ||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_CARD_CPROD}}||<math> \card (S \cprod  T) \;\;\defi\;\; \card (S) * \card (T) </math>|| ||  A
{{RRRow}}| ||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_CARD_CONVERSE}}||<math>  \card (r^{-1} ) \;\;\defi\;\;  \card (r) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_CONVERSE}}||<math>  \card (r^{-1} ) \;\;\defi\;\;  \card (r) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_ID}}||<math>  \card (\id (S)) \;\;\defi\;\;  \card (S) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_ID}}||<math>  \card (\id) \;\;\defi\;\;  \card (S) </math>|| where <math>\id</math> has type <math>\pow (S \cprod S) </math>||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_LAMBDA}}||<math>  \card (\lambda x\qdot (P \mid E)) \;\;\defi\;\;  \card (\{ x \qdot P \mid x\} ) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_ID_DOMRES}}||<math>  \card (S\domres\id) \;\;\defi\;\;  \card (S) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_COMPSET}}||<math> \card (\{ x \qdot x \in  S \mid  x\} ) \;\;\defi\;\; \card (S) </math>|| where <math>x</math> non free in <math>S</math> || A
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_CARD_PRJ1_DOMRES}}||<math>  \card (E \domres \prjone) \;\;\defi\;\;  \card (E) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_PRJ2_DOMRES}}||<math> \card (E \domres \prjtwo) \;\;\defi\;\; \card (E) </math>||  ||  A
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_LIT_GE_CARD_0}}||<math>  \card (S) \geq  1 \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_GE_CARD_1}}||<math>  \card (S) \geq  1 \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE_CARD_1}}||<math>  1 \leq  \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE_CARD_1}}||<math>  1 \leq  \card (S) \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE_CARD_0}}||<math>  0 \leq  \card (S) \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE_CARD_0}}||<math>  0 \leq  \card (S) \;\;\defi\;\;  \btrue </math>||  ||  A
Line 36: Line 44:
{{RRRow}}|*||{{Rulename|SIMP_CARD_NATURAL}}||<math>  \card (S) \in  \nat  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_NATURAL}}||<math>  \card (S) \in  \nat  \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_NATURAL1}}||<math>  \card (S) \in  \natn  \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_NATURAL1}}||<math>  \card (S) \in  \natn  \;\;\defi\;\;  \lnot\, S = \emptyset </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_NATURAL}}||<math>  i \in  \nat  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_NATURAL}}||<math>  i \in  \nat  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a non-negative literal ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_IN_NATURAL1}}||<math>  0 \in  \natn  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN_NATURAL1}}||<math>  0 \in  \natn  \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_NATURAL1}}||<math>  i \in  \natn  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a literal and <math>1 \leq i</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_NATURAL1}}||<math>  i \in  \natn  \;\;\defi\;\;  \btrue </math>|| where <math>i</math> is a positive literal ||  A
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_MINUS_NATURAL}}||<math>  -i \in  \nat  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a literal and <math>1 \leq i</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_MINUS_NATURAL}}||<math>  -i \in  \nat  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a positive literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_MINUS_NATURAL1}}||<math>  -i \in  \natn  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_IN_MINUS_NATURAL1}}||<math>  -i \in  \natn  \;\;\defi\;\;  \bfalse </math>|| where <math>i</math> is a non-negative literal ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math> \bool (\btrue ) \;\;\defi\;\;  \True </math>||  ||  A
{{RRRow}}|*||{{Rulename|DEF_IN_NATURAL}}||<math>x \in \nat  \;\;\defi\;\;  0 \leq x </math>||  ||  M
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math> \bool (\bfalse ) \;\;\defi\;\;  \False </math>||  ||  A
{{RRRow}}|*||{{Rulename|DEF_IN_NATURAL1}}||<math>x \in \natn  \;\;\defi\;\;  1 \leq x </math>||  ||  M
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_KBOOL_TRUE}}||<math>  \bool (P) = \True  \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_KBOOL_TRUE}}||<math>  \bool (P) = \True  \;\;\defi\;\;  P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_KBOOL_FALSE}}||<math>  \bool (P) = \False  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_KBOOL_FALSE}}||<math>  \bool (P) = \False  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_KBOOL_LIT_EQUAL_TRUE}}||<math> \bool (B = \True) \;\;\defi\;\; B </math>||  ||  A
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
Line 52: Line 61:
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MINUS_L}}||<math>  0 - E \;\;\defi\;\;  -E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MINUS_L}}||<math>  0 - E \;\;\defi\;\;  -E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MINUS_MINUS}}||<math>  - (- E) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MINUS_MINUS}}||<math>  - (- E) \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MINUS_UNMINUS}}||<math> E  - (- F) \;\;\defi\;\;  E + F </math>|| where <math>(-F)</math> is a unary minus expression or a negative literal ||  M
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MINUS}}||<math>  E - E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MINUS}}||<math>  E - E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MINUS_PLUS_L}}||<math> (A + \ldots + C + \ldots + B) - C \;\;\defi\;\; A + \ldots + B </math>|| ||  M
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MINUS_PLUS_R}}||<math> C - (A + \ldots + C + \ldots + B)  \;\;\defi\;\;  -(A + \ldots + B) </math>|| ||  M
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_MULTI_PLUS_MINUS}}||<math>(A + \ldots + D + \ldots + (C - D) + \ldots + B) \;\;\defi\;\; A + \ldots + C + \ldots + B  </math>|| ||  M
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|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
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_0}}||<math>  E * \ldots  * 0 * \ldots  * F \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_0}}||<math>  E * \ldots  * 0 * \ldots  * F \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_1}}||<math>  E * \ldots  * 1 * \ldots  * F \;\;\defi\;\;  E * \ldots  * F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_1}}||<math>  E * \ldots  * 1 * \ldots  * F \;\;\defi\;\;  E * \ldots  * F </math>||  ||  A
Line 58: Line 77:
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_MINUS_ODD}}||<math>  (-E) * \ldots  * (-F) \;\;\defi\;\;  -(E * \ldots  * F) </math>|| if an odd number of <math>-</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_MINUS_ODD}}||<math>  (-E) * \ldots  * (-F) \;\;\defi\;\;  -(E * \ldots  * F) </math>|| if an odd number of <math>-</math> ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MINUS}}||<math>  - (i) \;\;\defi\;\;  (-i) </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MINUS}}||<math>  - (i) \;\;\defi\;\;  (-i) </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_MINUS_MINUS}}||<math>  - (-i) \;\;\defi\;\;  i </math>|| where <math>i</math> is a literal ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL}}||<math>  i = j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL}}||<math>  i = j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE}}||<math>  i \leq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_LE}}||<math>  i \leq  j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
Line 65: Line 83:
{{RRRow}}|*||{{Rulename|SIMP_LIT_GT}}||<math>  i > j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_LIT_GT}}||<math>  i > j \;\;\defi\;\;  \btrue  \;or\; \bfalse  \;\;(computation) </math>|| where <math>i</math> and <math>j</math> are literals ||  A
{{RRRow}}|*||{{Rulename|SIMP_DIV_MINUS}}||<math>  (- E) \div  (-F) \;\;\defi\;\;  E \div  F </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_DIV_MINUS}}||<math>  (- E) \div  (-F) \;\;\defi\;\;  E \div  F </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DIV_1}}||<math>  E \div  1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DIV_1}}||<math>  E \div  1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DIV_0}}||<math>  0 \div  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DIV_0}}||<math>  0 \div  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_1_R}}||<math>  E ^ 1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_1_R}}||<math>  E ^ 1 \;\;\defi\;\;  E </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_1_L}}||<math>  1 ^ E \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_1_L}}||<math>  1 ^ E \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_0}}||<math>  E ^ 0 \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EXPN_0}}||<math>  E ^ 0 \;\;\defi\;\;  1 </math>||  ||  A
{{RRRow}}|*||{{Rulename|DEF_EXPN_STEP}}||<math> E ^ P \;\;\defi\;\; E * E ^{(P - 1)} </math>|| with an additional PO <math>\lnot\, P = 0</math> || M
{{RRRow}}|*||{{Rulename|SIMP_MULTI_LE}}||<math>  E \leq  E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_LE}}||<math>  E \leq  E \;\;\defi\;\;  \btrue </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_LT}}||<math>  E < E \;\;\defi\;\;  \bfalse </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_LT}}||<math>  E < E \;\;\defi\;\;  \bfalse </math>||  ||  A
Line 77: Line 96:
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DIV_PROD}}||<math>  (X * \ldots * E * \ldots * Y) \div  E \;\;\defi\;\;  X * \ldots * Y </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DIV_PROD}}||<math>  (X * \ldots * E * \ldots * Y) \div  E \;\;\defi\;\;  X * \ldots * Y </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MOD}}||<math>  E \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_MULTI_MOD}}||<math>  E \,\bmod\,  E \;\;\defi\;\;  0 </math>||  ||  A
{{RRRow}}|*||{{Rulename|DISTRI_PROD_PLUS}}||<math>  a * (b + c) \;\;\defi\;\;  (a * b) + (a * c) </math>||  ||  M
{{RRRow}}|||{{Rulename|DISTRI_PROD_PLUS}}||<math>  a * (b + c) \;\;\defi\;\;  (a * b) + (a * c) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DISTRI_PROD_MINUS}}||<math>  a * (b - c) \;\;\defi\;\;  (a * b) - (a * c) </math>||  ||  M
{{RRRow}}|||{{Rulename|DISTRI_PROD_MINUS}}||<math>  a * (b - c) \;\;\defi\;\;  (a * b) - (a * c) </math>||  ||  M
{{RRRow}}|*||{{Rulename|DERIV_LE_CARD}}||<math> \card (S) \leq  \card (T) \;\;\defi\;\;  S \subseteq  T </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}| ||{{Rulename|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  
{{RRRow}}|*||{{Rulename|DERIV_GE_CARD}}||<math>  \card (S) \geq  \card (T) \;\;\defi\;\;  T \subseteq  S </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||{{Rulename|DERIV_LT_CARD}}||<math>  \card (S) < \card (T) \;\;\defi\;\;  S  \subset  T </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||{{Rulename|DERIV_GT_CARD}}||<math>  \card (S) > \card (T) \;\;\defi\;\;  T  \subset  S </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M
{{RRRow}}|*||{{Rulename|DERIV_EQUAL_CARD}}||<math>  \card (S) = \card (T) \;\;\defi\;\;  S = T </math>|| <math>S</math> and <math>T</math> must be of the same type ||  M  
|}
|}


Latest revision as of 15:11, 3 June 2024

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
 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_MIN_IN
 \min (S) \in S \;\;\defi\;\; \btrue A
*
SIMP_MAX_IN
 \max (S) \in S \;\;\defi\;\; \btrue 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_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\expn{\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(T) with hypotheses T\subseteq S and either \finite(S) or \finite(T) A
SIMP_CARD_SETMINUS_SETENUM
 \card(S\setminus\{E_1,\ldots,E_n\})\;\;\defi\;\;\card(S) - \card(\{E_1,\ldots,E_n\}) with hypotheses E_i\in S for all i\in 1\upto n A
*
SIMP_CARD_CONVERSE
 \card (r^{-1} ) \;\;\defi\;\; \card (r) A
*
SIMP_CARD_ID
 \card (\id) \;\;\defi\;\; \card (S) where \id has type \pow (S \cprod S) A
*
SIMP_CARD_ID_DOMRES
 \card (S\domres\id) \;\;\defi\;\; \card (S) A
*
SIMP_CARD_PRJ1
 \card (\prjone) \;\;\defi\;\; \card (S \cprod T) where \prjone has type \pow(S \cprod T \cprod S) A
*
SIMP_CARD_PRJ2
 \card (\prjtwo) \;\;\defi\;\; \card (S \cprod T) where \prjtwo has type \pow(S \cprod T \cprod T) A
*
SIMP_CARD_PRJ1_DOMRES
 \card (E \domres \prjone) \;\;\defi\;\; \card (E) A
*
SIMP_CARD_PRJ2_DOMRES
 \card (E \domres \prjtwo) \;\;\defi\;\; \card (E) A
*
SIMP_CARD_LAMBDA
 \card(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \card(\{x\qdot P\mid E\} ) where E is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., E is syntactically injective) and all identifiers bound by the comprehension set that occur in F also occur in E 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_1
 \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 non-negative 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 positive literal 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 positive literal A
*
SIMP_LIT_IN_MINUS_NATURAL1
 -i \in \natn \;\;\defi\;\; \bfalse where i is a non-negative literal A
*
DEF_IN_NATURAL
 x \in \nat \;\;\defi\;\; 0 \leq x M
*
DEF_IN_NATURAL1
 x \in \natn \;\;\defi\;\; 1 \leq x M
*
SIMP_LIT_EQUAL_KBOOL_TRUE
 \bool (P) = \True \;\;\defi\;\; P A
*
SIMP_LIT_EQUAL_KBOOL_FALSE
 \bool (P) = \False \;\;\defi\;\; \lnot\, P A
*
SIMP_KBOOL_LIT_EQUAL_TRUE
 \bool (B = \True) \;\;\defi\;\; B 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_MINUS_UNMINUS
 E - (- F) \;\;\defi\;\; E + F where (-F) is a unary minus expression or a negative literal M
*
SIMP_MULTI_MINUS
 E - E \;\;\defi\;\; 0 A
*
SIMP_MULTI_MINUS_PLUS_L
 (A + \ldots + C + \ldots + B) - C \;\;\defi\;\; A + \ldots + B M
*
SIMP_MULTI_MINUS_PLUS_R
 C - (A + \ldots + C + \ldots + B) \;\;\defi\;\; -(A + \ldots + B) M
*
SIMP_MULTI_MINUS_PLUS_PLUS
 (A + \ldots + E + \ldots + B) - (C + \ldots + E + \ldots + D) \;\;\defi\;\; (A + \ldots + B) - (C + \ldots + D) M
*
SIMP_MULTI_PLUS_MINUS
 (A + \ldots + D + \ldots + (C - D) + \ldots + B) \;\;\defi\;\; A + \ldots + C + \ldots + B M
*
SIMP_MULTI_ARITHREL_PLUS_PLUS
 A + \ldots + E + \ldots + B < C + \ldots + E + \ldots + D \;\;\defi\;\; A + \ldots + B < C + \ldots + D where the root relation (< here) is one of \{=, <, \leq, >, \geq\} M
*
SIMP_MULTI_ARITHREL_PLUS_R
 C < A + \ldots + C \ldots + B \;\;\defi\;\; 0 < A + \ldots + B where the root relation (< here) is one of \{=, <, \leq, >, \geq\} M
*
SIMP_MULTI_ARITHREL_PLUS_L
 A + \ldots + C \ldots + B < C \;\;\defi\;\; A + \ldots + B < 0 where the root relation (< here) is one of \{=, <, \leq, >, \geq\} M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_R
 A - C < B - C \;\;\defi\;\; A < B where the root relation (< here) is one of \{=, <, \leq, >, \geq\} M
*
SIMP_MULTI_ARITHREL_MINUS_MINUS_L
 C - A < C - B \;\;\defi\;\; B < A where the root relation (< here) is one of \{=, <, \leq, >, \geq\} M
*
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_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
*
DEF_EXPN_STEP
 E ^ P \;\;\defi\;\; E * E ^{(P - 1)} with an additional PO \lnot\, P = 0 M
*
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_NOT_EQUAL
 \lnot E = F \;\;\defi\;\; E < F \lor E > F E and F must be of Integer type M
Retrieved from ‘https://wiki.event-b.org/index.php?title=Arithmetic_Rewrite_Rules&oldid=14561’