Arithmetic Rewrite Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
Guillaume (talk | contribs)
Add rule for exponentiation step
Guillaume (talk | contribs)
Rules DEF_EXPN_STEP, SIMP_{MIN,MAX}_IN and SIMP_KBOOL_LIT_EQUAL_TRUE have been implemented in Rodin 3.9
 
Line 14: 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_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_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
Line 54: Line 54:
{{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|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 88: 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|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

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