Difference between revisions of "Arithmetic Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Laurent m (Fixed rule names to make them easy to extract) |
(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_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 | + | {{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}}| | + | {{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}}| | + | {{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| | + | {{RRRow}}|*||{{Rulename|SIMP_CARD_ID_DOMRES}}||<math> \card (S\domres\id) \;\;\defi\;\; \card (S) </math>|| || A |
− | {{RRRow}}|*||{{Rulename| | + | {{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}}| | + | {{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| | + | {{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 | + | {{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 | + | {{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| | + | {{RRRow}}|*||{{Rulename|DEF_IN_NATURAL}}||<math>x \in \nat \;\;\defi\;\; 0 \leq x </math>|| || M |
− | {{RRRow}}| ||{{Rulename| | + | {{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_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}}| | + | {{RRRow}}|||{{Rulename|DISTRI_PROD_PLUS}}||<math> a * (b + c) \;\;\defi\;\; (a * b) + (a * c) </math>|| || M |
− | {{RRRow}}| | + | {{RRRow}}|||{{Rulename|DISTRI_PROD_MINUS}}||<math> a * (b - c) \;\;\defi\;\; (a * b) - (a * c) </math>|| || M |
− | {{RRRow}}| | + | {{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 |
− | |||
− | |||
− | |||
− | |||
|} | |} | ||
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 |
![]() |
A | |
* | SIMP_SPECIAL_MOD_1 |
![]() |
A | |
* | SIMP_MIN_SING |
![]() |
where ![]() |
A |
* | SIMP_MAX_SING |
![]() |
where ![]() |
A |
* | SIMP_MIN_NATURAL |
![]() |
A | |
* | SIMP_MIN_NATURAL1 |
![]() |
A | |
* | SIMP_MIN_BUNION_SING |
![]() |
A | |
* | SIMP_MAX_BUNION_SING |
![]() |
A | |
* | SIMP_MIN_UPTO |
![]() |
A | |
* | SIMP_MAX_UPTO |
![]() |
A | |
* | SIMP_MIN_IN |
![]() |
A | |
* | SIMP_MAX_IN |
![]() |
A | |
* | SIMP_LIT_MIN |
![]() |
where ![]() ![]() ![]() |
A |
* | SIMP_LIT_MAX |
![]() |
where ![]() ![]() ![]() |
A |
* | SIMP_SPECIAL_CARD |
![]() |
A | |
* | SIMP_CARD_SING |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_EQUAL_CARD |
![]() |
A | |
* | SIMP_CARD_POW |
![]() |
A | |
* | SIMP_CARD_BUNION |
![]() |
A | |
SIMP_CARD_SETMINUS |
![]() |
with hypotheses ![]() ![]() ![]() |
A | |
SIMP_CARD_SETMINUS_SETENUM |
![]() |
with hypotheses ![]() ![]() |
A | |
* | SIMP_CARD_CONVERSE |
![]() |
A | |
* | SIMP_CARD_ID |
![]() |
where ![]() ![]() |
A |
* | SIMP_CARD_ID_DOMRES |
![]() |
A | |
* | SIMP_CARD_PRJ1 |
![]() |
where ![]() ![]() |
A |
* | SIMP_CARD_PRJ2 |
![]() |
where ![]() ![]() |
A |
* | SIMP_CARD_PRJ1_DOMRES |
![]() |
A | |
* | SIMP_CARD_PRJ2_DOMRES |
![]() |
A | |
* | SIMP_CARD_LAMBDA |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | SIMP_LIT_CARD_UPTO |
![]() |
where ![]() ![]() ![]() |
A |
SIMP_TYPE_CARD |
![]() |
where ![]() ![]() |
A | |
* | SIMP_LIT_GE_CARD_1 |
![]() |
A | |
* | SIMP_LIT_LE_CARD_1 |
![]() |
A | |
* | SIMP_LIT_LE_CARD_0 |
![]() |
A | |
* | SIMP_LIT_GE_CARD_0 |
![]() |
A | |
* | SIMP_LIT_GT_CARD_0 |
![]() |
A | |
* | SIMP_LIT_LT_CARD_0 |
![]() |
A | |
* | SIMP_LIT_EQUAL_CARD_1 |
![]() |
A | |
* | SIMP_CARD_NATURAL |
![]() |
A | |
* | SIMP_CARD_NATURAL1 |
![]() |
A | |
* | SIMP_LIT_IN_NATURAL |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_IN_NATURAL1 |
![]() |
A | |
* | SIMP_LIT_IN_NATURAL1 |
![]() |
where ![]() |
A |
* | SIMP_LIT_UPTO |
![]() |
where ![]() ![]() ![]() |
A |
* | SIMP_LIT_IN_MINUS_NATURAL |
![]() |
where ![]() |
A |
* | SIMP_LIT_IN_MINUS_NATURAL1 |
![]() |
where ![]() |
A |
* | DEF_IN_NATURAL |
![]() |
M | |
* | DEF_IN_NATURAL1 |
![]() |
M | |
* | SIMP_LIT_EQUAL_KBOOL_TRUE |
![]() |
A | |
* | SIMP_LIT_EQUAL_KBOOL_FALSE |
![]() |
A | |
* | SIMP_KBOOL_LIT_EQUAL_TRUE |
![]() |
A | |
* | DEF_EQUAL_MIN |
![]() |
where ![]() ![]() |
M |
* | DEF_EQUAL_MAX |
![]() |
where ![]() ![]() |
M |
* | SIMP_SPECIAL_PLUS |
![]() |
A | |
* | SIMP_SPECIAL_MINUS_R |
![]() |
A | |
* | SIMP_SPECIAL_MINUS_L |
![]() |
A | |
* | SIMP_MINUS_MINUS |
![]() |
A | |
* | SIMP_MINUS_UNMINUS |
![]() |
where ![]() |
M |
* | SIMP_MULTI_MINUS |
![]() |
A | |
* | SIMP_MULTI_MINUS_PLUS_L |
![]() |
M | |
* | SIMP_MULTI_MINUS_PLUS_R |
![]() |
M | |
* | SIMP_MULTI_MINUS_PLUS_PLUS |
![]() |
M | |
* | SIMP_MULTI_PLUS_MINUS |
![]() |
M | |
* | SIMP_MULTI_ARITHREL_PLUS_PLUS |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_PLUS_R |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_PLUS_L |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_R |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_L |
![]() |
where the root relation (![]() ![]() |
M |
* | SIMP_SPECIAL_PROD_0 |
![]() |
A | |
* | SIMP_SPECIAL_PROD_1 |
![]() |
A | |
* | SIMP_SPECIAL_PROD_MINUS_EVEN |
![]() |
if an even number of ![]() |
A |
* | SIMP_SPECIAL_PROD_MINUS_ODD |
![]() |
if an odd number of ![]() |
A |
* | SIMP_LIT_MINUS |
![]() |
where ![]() |
A |
* | SIMP_LIT_EQUAL |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_LE |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_LT |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_GE |
![]() |
where ![]() ![]() |
A |
* | SIMP_LIT_GT |
![]() |
where ![]() ![]() |
A |
* | SIMP_DIV_MINUS |
![]() |
A | |
* | SIMP_SPECIAL_DIV_1 |
![]() |
A | |
* | SIMP_SPECIAL_DIV_0 |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_1_R |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_1_L |
![]() |
A | |
* | SIMP_SPECIAL_EXPN_0 |
![]() |
A | |
* | DEF_EXPN_STEP |
![]() |
with an additional PO ![]() |
M |
* | SIMP_MULTI_LE |
![]() |
A | |
* | SIMP_MULTI_LT |
![]() |
A | |
* | SIMP_MULTI_GE |
![]() |
A | |
* | SIMP_MULTI_GT |
![]() |
A | |
* | SIMP_MULTI_DIV |
![]() |
A | |
* | SIMP_MULTI_DIV_PROD |
![]() |
A | |
* | SIMP_MULTI_MOD |
![]() |
A | |
DISTRI_PROD_PLUS |
![]() |
M | ||
DISTRI_PROD_MINUS |
![]() |
M | ||
DERIV_NOT_EQUAL |
![]() |
![]() ![]() |
M |