Difference between revisions of "Arithmetic Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Laurent (Removed rules SIMP_CARD_SETMINUS and SIMP_CARD_CPROD (are now inference rules).) |
(Rules DEF_EXPN_STEP, SIMP_{MIN,MAX}_IN and SIMP_KBOOL_LIT_EQUAL_TRUE have been implemented in Rodin 3.9) |
||
(22 intermediate revisions by 5 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 |
− | {{RRRow}}|||{{Rulename|SIMP_MIN_NATURAL}}||<math> \min (\nat ) \;\;\defi\;\; 0 </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_MIN_NATURAL}}||<math> \min (\nat ) \;\;\defi\;\; 0 </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_MIN_NATURAL1}}||<math> \min (\natn ) \;\;\defi\;\; 1 </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_MIN_NATURAL1}}||<math> \min (\natn ) \;\;\defi\;\; 1 </math>|| || A |
− | {{RRRow}}|||{{Rulename|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 | + | {{RRRow}}|*||{{Rulename|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 |
− | {{RRRow}}|||{{Rulename|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 | + | {{RRRow}}|*||{{Rulename|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 |
− | {{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| | + | {{RRRow}}|*||{{Rulename|SIMP_MIN_IN}}||<math> \min (S) \in S \;\;\defi\;\; \btrue </math>|| || A |
− | {{RRRow}}|||{{Rulename| | + | {{RRRow}}|*||{{Rulename|SIMP_MAX_IN}}||<math> \max (S) \in S \;\;\defi\;\; \btrue </math>|| || A |
− | {{RRRow}}|||{{Rulename| | + | {{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_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}}|||{{Rulename|SIMP_CARD_CONVERSE}}||<math> \card (r^{-1} ) \;\;\defi\;\; \card (r) </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_ID}}||<math> \card (\id (S)) \;\;\defi\;\; \card (S) </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| | + | {{RRRow}}|*||{{Rulename|SIMP_CARD_CONVERSE}}||<math> \card (r^{-1} ) \;\;\defi\;\; \card (r) </math>|| || A |
− | {{RRRow}}|||{{Rulename| | + | {{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_ID_DOMRES}}||<math> \card (S\domres\id) \;\;\defi\;\; \card (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| | + | {{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 |
− | {{RRRow}}|||{{Rulename|SIMP_LIT_GE_CARD_0}}||<math> \card (S) \geq 0 \;\;\defi\;\; \btrue </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_LIT_GE_CARD_0}}||<math> \card (S) \geq 0 \;\;\defi\;\; \btrue </math>|| || A |
{{RRRow}}|*||{{Rulename|SIMP_LIT_GT_CARD_0}}||<math> \card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_LIT_GT_CARD_0}}||<math> \card (S) > 0 \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_LIT_LT_CARD_0}}||<math> 0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_LIT_LT_CARD_0}}||<math> 0 < \card (S) \;\;\defi\;\; \lnot\, S = \emptyset </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_CARD_1}}||<math> \card (S) = 1 \;\;\defi\;\; \exists x \qdot S = \{ x\} </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_LIT_EQUAL_CARD_1}}||<math> \card (S) = 1 \;\;\defi\;\; \exists x \qdot S = \{ x\} </math>|| || A | ||
− | {{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 non-negative 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 positive literal || 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 positive literal || 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 non-negative 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|DEF_IN_NATURAL}}||<math>x \in \nat \;\;\defi\;\; 0 \leq x </math>|| | + | {{RRRow}}|*||{{Rulename|DEF_IN_NATURAL}}||<math>x \in \nat \;\;\defi\;\; 0 \leq x </math>|| || M |
− | {{RRRow}}| ||{{Rulename|DEF_IN_NATURAL1}}||<math>x \in \natn \;\;\defi\;\; 1 \leq x | + | {{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|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|SIMP_KBOOL_LIT_EQUAL_TRUE}}||<math> \bool (B = \True) \;\;\defi\;\; B </math>|| || A |
− | {{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_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|SIMP_SPECIAL_PLUS}}||<math> E + \ldots + 0 + \ldots + F \;\;\defi\;\; E + \ldots + F </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PLUS}}||<math> E + \ldots + 0 + \ldots + F \;\;\defi\;\; E + \ldots + F </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MINUS_R}}||<math> E - 0 \;\;\defi\;\; E </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_MINUS_R}}||<math> E - 0 \;\;\defi\;\; E </math>|| || A | ||
Line 67: | Line 76: | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_MINUS_EVEN}}||<math> (-E) * \ldots * (-F) \;\;\defi\;\; E * \ldots * F </math>|| if an even number of <math>-</math> || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_PROD_MINUS_EVEN}}||<math> (-E) * \ldots * (-F) \;\;\defi\;\; E * \ldots * F </math>|| if an even 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_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) | + | {{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 75: | 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 86: | Line 95: | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DIV}}||<math> E \div E \;\;\defi\;\; 1 </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_MULTI_DIV}}||<math> E \div E \;\;\defi\;\; 1 </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_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 |
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 is a single expression | A | |
* | SIMP_MAX_SING |
where is a single expression | 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 and are literals and | A | |
* | SIMP_LIT_MAX |
where and are literals and | A | |
* | SIMP_SPECIAL_CARD |
A | ||
* | SIMP_CARD_SING |
where is a single expression | A | |
* | SIMP_SPECIAL_EQUAL_CARD |
A | ||
* | SIMP_CARD_POW |
A | ||
* | SIMP_CARD_BUNION |
A | ||
SIMP_CARD_SETMINUS |
with hypotheses and either or | A | ||
SIMP_CARD_SETMINUS_SETENUM |
with hypotheses for all | A | ||
* | SIMP_CARD_CONVERSE |
A | ||
* | SIMP_CARD_ID |
where has type | A | |
* | SIMP_CARD_ID_DOMRES |
A | ||
* | SIMP_CARD_PRJ1 |
where has type | A | |
* | SIMP_CARD_PRJ2 |
where has type | A | |
* | SIMP_CARD_PRJ1_DOMRES |
A | ||
* | SIMP_CARD_PRJ2_DOMRES |
A | ||
* | SIMP_CARD_LAMBDA |
where is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., is syntactically injective) and all identifiers bound by the comprehension set that occur in also occur in | A | |
* | SIMP_LIT_CARD_UPTO |
where and are literals and | A | |
SIMP_TYPE_CARD |
where is a carrier set containing elements | 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 is a non-negative literal | A | |
* | SIMP_SPECIAL_IN_NATURAL1 |
A | ||
* | SIMP_LIT_IN_NATURAL1 |
where is a positive literal | A | |
* | SIMP_LIT_UPTO |
where and are literals and | A | |
* | SIMP_LIT_IN_MINUS_NATURAL |
where is a positive literal | A | |
* | SIMP_LIT_IN_MINUS_NATURAL1 |
where is a non-negative literal | 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 non free in | M | |
* | DEF_EQUAL_MAX |
where non free in | M | |
* | SIMP_SPECIAL_PLUS |
A | ||
* | SIMP_SPECIAL_MINUS_R |
A | ||
* | SIMP_SPECIAL_MINUS_L |
A | ||
* | SIMP_MINUS_MINUS |
A | ||
* | SIMP_MINUS_UNMINUS |
where is a unary minus expression or a negative literal | 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 ( here) is one of | M | |
* | SIMP_MULTI_ARITHREL_PLUS_R |
where the root relation ( here) is one of | M | |
* | SIMP_MULTI_ARITHREL_PLUS_L |
where the root relation ( here) is one of | M | |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_R |
where the root relation ( here) is one of | M | |
* | SIMP_MULTI_ARITHREL_MINUS_MINUS_L |
where the root relation ( here) is one of | 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 is a literal | A | |
* | SIMP_LIT_EQUAL |
where and are literals | A | |
* | SIMP_LIT_LE |
where and are literals | A | |
* | SIMP_LIT_LT |
where and are literals | A | |
* | SIMP_LIT_GE |
where and are literals | A | |
* | SIMP_LIT_GT |
where and are literals | 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 |
and must be of Integer type | M |