Set Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Laurent Removed rules SIMP_SPECIAL_FORALL_BTRUE, SIMP_SPECIAL_FORALL_BFALSE, SIMP_SPECIAL_EXISTS_BTRUE, and SIMP_SPECIAL_EXISTS_BFALSE which are subsumed by SIMP_FORALL and SIMP_EXISTS respectively. |
imported>Laurent Removed rules about overriding which belong to set rewrite. |
||
Line 96: | Line 96: | ||
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET_ONEPOINT}}||<math> E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E) </math>|| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate || A | {{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET_ONEPOINT}}||<math> E \in \{ x \qdot P(x) \mid x \} \;\;\defi\;\; P(E) </math>|| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate || A | ||
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_R}}||<math> S \subseteq \{ x \qdot P(x) \mid x \} \;\;\defi\;\; \forall y\qdot y \in S \limp P(y) </math>|| where <math>y</math> non free in <math>S, \{ x \qdot P(x) \mid x \}</math> || A | {{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_R}}||<math> S \subseteq \{ x \qdot P(x) \mid x \} \;\;\defi\;\; \forall y\qdot y \in S \limp P(y) </math>|| where <math>y</math> non free in <math>S, \{ x \qdot P(x) \mid x \}</math> || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BTRUE}}||<math> \bool (\btrue ) \;\;\defi\;\; \True </math>|| || A | {{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_SPECIAL_KBOOL_BFALSE}}||<math> \bool (\bfalse ) \;\;\defi\;\; \False </math>|| || A |
Revision as of 13:13, 27 October 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_AND_BTRUE |
A | ||
* | SIMP_SPECIAL_AND_BFALSE |
A | ||
* | SIMP_MULTI_AND |
A | ||
* | SIMP_MULTI_AND_NOT |
A | ||
* | SIMP_SPECIAL_OR_BTRUE |
A | ||
* | SIMP_SPECIAL_OR_BFALSE |
A | ||
* | SIMP_MULTI_OR |
A | ||
* | SIMP_MULTI_OR_NOT |
A | ||
* | SIMP_SPECIAL_IMP_BTRUE_R |
A | ||
* | SIMP_SPECIAL_IMP_BTRUE_L |
A | ||
* | SIMP_SPECIAL_IMP_BFALSE_R |
A | ||
* | SIMP_SPECIAL_IMP_BFALSE_L |
A | ||
* | SIMP_MULTI_IMP |
A | ||
SIMP_MULTI_IMP_OR |
A | |||
SIMP_MULTI_IMP_AND_NOT_R |
A | |||
SIMP_MULTI_IMP_AND_NOT_L |
A | |||
* | SIMP_MULTI_EQV |
A | ||
SIMP_MULTI_EQV_NOT |
A | |||
* | SIMP_SPECIAL_NOT_BTRUE |
A | ||
* | SIMP_SPECIAL_NOT_BFALSE |
A | ||
* | SIMP_NOT_NOT |
A | ||
* | SIMP_NOTEQUAL |
A | ||
* | SIMP_NOTIN |
A | ||
* | SIMP_NOTSUBSET |
A | ||
* | SIMP_NOTSUBSETEQ |
A | ||
* | SIMP_NOT_LE |
A | ||
* | SIMP_NOT_GE |
A | ||
* | SIMP_NOT_LT |
A | ||
* | SIMP_NOT_GT |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_FALSE_R |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_FALSE_L |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_TRUE_R |
A | ||
* | SIMP_SPECIAL_NOT_EQUAL_TRUE_L |
A | ||
* | SIMP_FORALL_AND |
A | ||
* | SIMP_EXISTS_OR |
A | ||
* | SIMP_FORALL |
Quantified identifiers other than do not occur in | A | |
* | SIMP_EXISTS |
Quantified identifiers other than do not occur in | A | |
* | SIMP_MULTI_EQUAL |
A | ||
* | SIMP_MULTI_NOTEQUAL |
A | ||
* | SIMP_EQUAL_MAPSTO |
A | ||
* | SIMP_EQUAL_SING |
A | ||
* | SIMP_SPECIAL_EQUAL_TRUE |
A | ||
* | SIMP_TYPE_SUBSETEQ |
where is a type expression | A | |
SIMP_SUBSETEQ_SING |
where is a single expression | A | ||
* | SIMP_SPECIAL_SUBSETEQ |
A | ||
* | SIMP_MULTI_SUBSETEQ |
A | ||
* | SIMP_SUBSETEQ_BUNION |
A | ||
* | SIMP_SUBSETEQ_BINTER |
A | ||
* | DERIV_SUBSETEQ_BUNION |
M | ||
* | DERIV_SUBSETEQ_BINTER |
M | ||
* | SIMP_SPECIAL_IN |
A | ||
* | SIMP_MULTI_IN |
A | ||
* | SIMP_IN_SING |
A | ||
* | SIMP_MULTI_SETENUM |
A | ||
* | SIMP_SPECIAL_BINTER |
A | ||
* | SIMP_TYPE_BINTER |
where is a type expression | A | |
* | SIMP_MULTI_BINTER |
A | ||
SIMP_MULTI_EQUAL_BINTER |
A | |||
* | SIMP_SPECIAL_BUNION |
A | ||
* | SIMP_TYPE_BUNION |
where is a type expression | A | |
* | SIMP_MULTI_BUNION |
A | ||
SIMP_MULTI_EQUAL_BUNION |
A | |||
* | SIMP_MULTI_SETMINUS |
A | ||
* | SIMP_SPECIAL_SETMINUS_R |
A | ||
* | SIMP_SPECIAL_SETMINUS_L |
A | ||
* | SIMP_TYPE_SETMINUS |
where is a type expression | A | |
* | SIMP_TYPE_SETMINUS_SETMINUS |
where is a type expression | A | |
SIMP_TYPE_KUNION |
where is a type expression and | A | ||
SIMP_KUNION_POW |
A | |||
SIMP_KUNION_POW1 |
A | |||
SIMP_SPECIAL_KUNION |
A | |||
SIMP_SPECIAL_QUNION |
A | |||
SIMP_SPECIAL_KINTER |
A | |||
SIMP_TYPE_KINTER |
where is a type expression | A | ||
SIMP_SPECIAL_POW |
A | |||
SIMP_SPECIAL_POW1 |
A | |||
SIMP_SPECIAL_CPROD_R |
A | |||
SIMP_SPECIAL_CPROD_L |
A | |||
SIMP_COMPSET_EQUAL |
where non free in | A | ||
SIMP_COMPSET_IN |
where non free in | A | ||
c | SIMP_SPECIAL_COMPSET_BFALSE |
A | ||
SIMP_SPECIAL_COMPSET_BTRUE |
where the type of is | A | ||
SIMP_SUBSETEQ_COMPSET_L |
where is fresh | A | ||
SIMP_SPECIAL_EQUAL_COMPSET |
A | |||
* | SIMP_IN_COMPSET |
where , , are not free in | A | |
* | SIMP_IN_COMPSET_ONEPOINT |
Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate | A | |
SIMP_SUBSETEQ_COMPSET_R |
where non free in | A | ||
* | SIMP_SPECIAL_KBOOL_BTRUE |
A | ||
* | SIMP_SPECIAL_KBOOL_BFALSE |
A | ||
DISTRI_SUBSETEQ_BUNION_SING |
where is a single expression | M | ||
DEF_FINITE |
M | |||
* | SIMP_SPECIAL_FINITE |
A | ||
* | SIMP_FINITE_SETENUM |
A | ||
* | SIMP_FINITE_BUNION |
A | ||
* | SIMP_FINITE_POW |
A | ||
* | DERIV_FINITE_CPROD |
A | ||
* | SIMP_FINITE_CONVERSE |
A | ||
* | SIMP_FINITE_UPTO |
A | ||
SIMP_FINITE_ID |
where has type | A | ||
SIMP_FINITE_NATURAL |
A | |||
SIMP_FINITE_NATURAL1 |
A | |||
SIMP_FINITE_INTEGER |
A | |||
SIMP_FINITE_LAMBDA |
A | |||
* | SIMP_TYPE_EQUAL_EMPTY |
where is a type expression | A | |
* | SIMP_TYPE_IN |
where is a type expression | A | |
* | SIMP_SPECIAL_EQV_BTRUE |
A | ||
* | SIMP_SPECIAL_EQV_BFALSE |
A | ||
* | DEF_SUBSET |
A | ||
SIMP_SPECIAL_SUBSET_R |
A | |||
SIMP_SPECIAL_SUBSET_L |
A | |||
* | SIMP_TYPE_SUBSET_L |
where is a type expression | A | |
SIMP_MULTI_SUBSET |
A | |||
* | SIMP_EQUAL_CONSTR |
where is a datatype constructor | A | |
* | SIMP_EQUAL_CONSTR_DIFF |
where and are different datatype constructors | A | |
* | SIMP_DESTR_CONSTR |
where is the datatype destructor for the i-th argument of datatype constructor | A | |
* | DISTRI_AND_OR |
M | ||
* | DISTRI_OR_AND |
M | ||
* | DEF_OR |
M | ||
* | DERIV_IMP |
M | ||
* | DERIV_IMP_IMP |
M | ||
* | DISTRI_IMP_AND |
M | ||
* | DISTRI_IMP_OR |
M | ||
* | DEF_EQV |
M | ||
* | DISTRI_NOT_AND |
M | ||
* | DISTRI_NOT_OR |
M | ||
* | DERIV_NOT_IMP |
M | ||
* | DERIV_NOT_FORALL |
M | ||
* | DERIV_NOT_EXISTS |
M | ||
* | DEF_SPECIAL_NOT_EQUAL |
where is not free in | M | |
* | DEF_IN_MAPSTO |
M | ||
* | DEF_IN_POW |
M | ||
* | DEF_IN_POW1 |
M | ||
* | DEF_SUBSETEQ |
where is not free in or | M | |
* | DEF_IN_BUNION |
M | ||
* | DEF_IN_BINTER |
M | ||
* | DEF_IN_SETMINUS |
M | ||
* | DEF_IN_SETENUM |
M | ||
* | DEF_IN_KUNION |
where is fresh | M | |
* | DEF_IN_QUNION |
where is fresh | M | |
* | DEF_IN_KINTER |
where is fresh | M | |
* | DEF_IN_QINTER |
where is fresh | M | |
* | DEF_IN_UPTO |
M | ||
* | DISTRI_BUNION_BINTER |
M | ||
* | DISTRI_BINTER_BUNION |
M | ||
DISTRI_BINTER_SETMINUS |
M | |||
DISTRI_SETMINUS_BUNION |
M | |||
* | DERIV_TYPE_SETMINUS_BINTER |
where is a type expression | M | |
* | DERIV_TYPE_SETMINUS_BUNION |
where is a type expression | M | |
* | DERIV_TYPE_SETMINUS_SETMINUS |
where is a type expression | M | |
DISTRI_CPROD_BINTER |
M | |||
DISTRI_CPROD_BUNION |
M | |||
DISTRI_CPROD_SETMINUS |
M | |||
* | DERIV_SUBSETEQ |
where is the type of and | M | |
* | DERIV_EQUAL |
where is the type of and | M | |
* | DERIV_SUBSETEQ_SETMINUS_L |
M | ||
* | DERIV_SUBSETEQ_SETMINUS_R |
M | ||
* | DEF_PARTITION |
AM |