Arithmetic Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Laurent
m Marked rule SIMP_SPECIAL_DIV_1 as implemented
Guillaume (talk | contribs)
Rules DEF_EXPN_STEP, SIMP_{MIN,MAX}_IN and SIMP_KBOOL_LIT_EQUAL_TRUE have been implemented in Rodin 3.9
 
(19 intermediate revisions by 3 users not shown)
Line 4: Line 4:


{{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|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_MIN_IN}}||<math>  \min (S) \in S \;\;\defi\;\;  \btrue </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_MAX_IN}}||<math> \max (S) \in S \;\;\defi\;\;  \btrue </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_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_UPTO}}||<math> \max (\{ i, \ldots  , j\} ) \;\;\defi\;\;  A \;\;(computation) </math>|| where <math>i, ... ,\,j</math> are literals ||  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 ^ \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_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|SIMP_CARD_LAMBDA}}||<math>  \card (\lambda x\qdot (P \mid E)) \;\;\defi\;\;  \card (\{ x \qdot P \mid x\} ) </math>||  ||  A
{{RRRow}}|*||{{Rulename|SIMP_CARD_CONVERSE}}||<math>  \card (r^{-1} ) \;\;\defi\;\;  \card (r) </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_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|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
{{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>||  ||  M
{{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 </math>||  ||  M
{{RRRow}}|*||{{Rulename|DEF_IN_NATURAL1}}||<math>x \in \natn  \;\;\defi\;\;  1 \leq x </math>||  ||  M
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math>  \bool (\btrue ) \;\;\defi\;\;  \True </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math>  \bool (\bfalse ) \;\;\defi\;\;  \False </math>||  ||  A
{{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 71: 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) </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 84: Line 88:
{{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 90: 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
  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