Arithmetic Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas mNo edit summary |
imported>Laurent m Marked rule SIMP_SPECIAL_DIV_1 as implemented |
||
Line 79: | Line 79: | ||
{{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 |
Revision as of 14:39, 16 November 2010
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_LIT_MIN |
where and are literals and | A | ||
SIMP_LIT_MAX |
where and are literals and | A | ||
SIMP_LIT_MIN_UPTO |
where are literals | A | ||
SIMP_LIT_MAX_UPTO |
where are literals | 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_CONVERSE |
A | |||
SIMP_CARD_ID |
A | |||
SIMP_CARD_LAMBDA |
A | |||
SIMP_CARD_COMPSET |
where non free 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_0 |
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_SPECIAL_KBOOL_BTRUE |
A | |||
SIMP_SPECIAL_KBOOL_BFALSE |
A | |||
* | SIMP_LIT_EQUAL_KBOOL_TRUE |
A | ||
* | SIMP_LIT_EQUAL_KBOOL_FALSE |
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_MINUS_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 | ||
* | 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 |