Difference between revisions of "Set Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Laurent (Marked some rules as implemented) |
imported>Laurent (Add rules SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION) |
||
(4 intermediate revisions by 2 users not shown) | |||
Line 94: | Line 94: | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BTRUE}}||<math> \{ x \qdot \btrue \mid E \} \;\;\defi\;\; \mathit{Ty} </math>|| where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BTRUE}}||<math> \{ x \qdot \btrue \mid E \} \;\;\defi\;\; \mathit{Ty} </math>|| where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math> \{ x \qdot P(x) \mid E(x) \} \subseteq S \;\;\defi\;\; \forall y\qdot P(y) \limp E(y) \in S </math>|| where <math>y</math> is fresh || A | {{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math> \{ x \qdot P(x) \mid E(x) \} \subseteq S \;\;\defi\;\; \forall y\qdot P(y) \limp E(y) \in S </math>|| where <math>y</math> is fresh || A | ||
− | |||
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET}}||<math> F \in \{ x,y,\ldots \qdot P(x,y,\ldots) \mid E(x,y,\ldots) \} \;\;\defi\;\; \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math>|| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> || A | {{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET}}||<math> F \in \{ x,y,\ldots \qdot P(x,y,\ldots) \mid E(x,y,\ldots) \} \;\;\defi\;\; \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math>|| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> || 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_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 | ||
Line 144: | Line 143: | ||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_BOOL}}||<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_FINITE_BOOL}}||<math> \finite (\Bool ) \;\;\defi\;\; \btrue </math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_FINITE_LAMBDA}}||<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{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_FINITE_LAMBDA}}||<math> \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\; \finite(\{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_TYPE_IN}}||<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_IN}}||<math> t \in \mathit{Ty} \;\;\defi\;\; \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BTRUE}}||<math> P \leqv \btrue \;\;\defi\;\; P </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BTRUE}}||<math> P \leqv \btrue \;\;\defi\;\; P </math>|| || A | ||
Line 169: | Line 167: | ||
{{RRRow}}|*||{{Rulename|DERIV_NOT_FORALL}}||<math> \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P </math>|| || M | {{RRRow}}|*||{{Rulename|DERIV_NOT_FORALL}}||<math> \lnot\, \forall x \qdot P \;\;\defi\;\; \exists x \qdot \lnot\, P </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DERIV_NOT_EXISTS}}||<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>|| || M | {{RRRow}}|*||{{Rulename|DERIV_NOT_EXISTS}}||<math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall x \qdot \lnot\, P </math>|| || M | ||
− | + | {{RRRow}}|*||{{Rulename|DEF_IN_MAPSTO}}||<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>|| || AM | |
− | {{RRRow}}|*||{{Rulename|DEF_IN_MAPSTO}}||<math> E \mapsto F \in S \cprod T \;\;\defi\;\; E \in S \land F \in T </math>|| || | ||
{{RRRow}}|*||{{Rulename|DEF_IN_POW}}||<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_POW}}||<math> E \in \pow (S) \;\;\defi\;\; E \subseteq S </math>|| || M | ||
{{RRRow}}|*||{{Rulename|DEF_IN_POW1}}||<math> E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset </math>|| || M | {{RRRow}}|*||{{Rulename|DEF_IN_POW1}}||<math> E \in \pown (S) \;\;\defi\;\; E \in \pow (S) \land S \neq \emptyset </math>|| || M | ||
Line 206: | Line 203: | ||
\land& s_{n-1}\binter s_n = \emptyset | \land& s_{n-1}\binter s_n = \emptyset | ||
\end{array}</math>|| || AM | \end{array}</math>|| || AM | ||
+ | {{RRRow}}| ||{{Rulename|SIMP_EMPTY_PARTITION}}||<math>\operatorname{partition}(S) \;\;\defi\;\; S = \emptyset </math>|| || A | ||
+ | {{RRRow}}| ||{{Rulename|SIMP_SINGLE_PARTITION}}||<math>\operatorname{partition}(S, T) \;\;\defi\;\; S = T </math>|| || A | ||
|} | |} | ||
Revision as of 17:16, 2 October 2013
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_NOT_L |
![]() |
A | |
* | SIMP_MULTI_IMP_NOT_R |
![]() |
A | |
* | SIMP_MULTI_IMP_AND |
![]() |
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 |
![]() |
AM | |
* | 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_EXISTS_IMP |
![]() |
A | |
* | SIMP_FORALL |
![]() |
Quantified identifiers other than ![]() ![]() |
A |
* | SIMP_EXISTS |
![]() |
Quantified identifiers other than ![]() ![]() |
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 ![]() |
A |
* | SIMP_SUBSETEQ_SING |
![]() |
where ![]() |
A |
* | SIMP_SPECIAL_SUBSETEQ |
![]() |
A | |
* | SIMP_MULTI_SUBSETEQ |
![]() |
A | |
* | SIMP_SUBSETEQ_BUNION |
![]() |
A | |
* | SIMP_SUBSETEQ_BINTER |
![]() |
A | |
* | DERIV_SUBSETEQ_BUNION |
![]() |
A | |
* | DERIV_SUBSETEQ_BINTER |
![]() |
A | |
* | SIMP_SPECIAL_IN |
![]() |
A | |
* | SIMP_MULTI_IN |
![]() |
A | |
* | SIMP_IN_SING |
![]() |
A | |
* | SIMP_MULTI_SETENUM |
![]() |
A | |
* | SIMP_SPECIAL_BINTER |
![]() |
A | |
* | SIMP_TYPE_BINTER |
![]() |
where ![]() |
A |
* | SIMP_MULTI_BINTER |
![]() |
A | |
* | SIMP_MULTI_EQUAL_BINTER |
![]() |
A | |
* | SIMP_SPECIAL_BUNION |
![]() |
A | |
* | SIMP_TYPE_BUNION |
![]() |
where ![]() |
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 ![]() |
A |
* | SIMP_TYPE_SETMINUS_SETMINUS |
![]() |
where ![]() |
A |
* | SIMP_KUNION_POW |
![]() |
A | |
* | SIMP_KUNION_POW1 |
![]() |
A | |
* | SIMP_SPECIAL_KUNION |
![]() |
A | |
* | SIMP_SPECIAL_QUNION |
![]() |
A | |
* | SIMP_SPECIAL_KINTER |
![]() |
A | |
* | SIMP_KINTER_POW |
![]() |
A | |
* | SIMP_SPECIAL_POW |
![]() |
A | |
* | SIMP_SPECIAL_POW1 |
![]() |
A | |
* | SIMP_SPECIAL_CPROD_R |
![]() |
A | |
* | SIMP_SPECIAL_CPROD_L |
![]() |
A | |
SIMP_COMPSET_EQUAL |
![]() |
where ![]() ![]() ![]() |
A | |
* | SIMP_COMPSET_IN |
![]() |
where ![]() ![]() |
A |
* | SIMP_COMPSET_SUBSETEQ |
![]() |
where ![]() ![]() |
A |
* | SIMP_SPECIAL_COMPSET_BFALSE |
![]() |
A | |
* | SIMP_SPECIAL_COMPSET_BTRUE |
![]() |
where the type of ![]() ![]() ![]() |
A |
* | SIMP_SUBSETEQ_COMPSET_L |
![]() |
where ![]() |
A |
* | SIMP_IN_COMPSET |
![]() |
where ![]() ![]() ![]() ![]() |
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 ![]() ![]() |
M | |
* | SIMP_SPECIAL_OVERL |
![]() |
A | |
* | SIMP_SPECIAL_KBOOL_BTRUE |
![]() |
A | |
* | SIMP_SPECIAL_KBOOL_BFALSE |
![]() |
A | |
DISTRI_SUBSETEQ_BUNION_SING |
![]() |
where ![]() |
M | |
* | DEF_FINITE |
![]() |
M | |
* | SIMP_SPECIAL_FINITE |
![]() |
A | |
* | SIMP_FINITE_SETENUM |
![]() |
A | |
* | SIMP_FINITE_BUNION |
![]() |
A | |
SIMP_FINITE_UNION |
![]() |
M | ||
SIMP_FINITE_QUNION |
![]() |
M | ||
* | SIMP_FINITE_POW |
![]() |
A | |
* | DERIV_FINITE_CPROD |
![]() |
A | |
* | SIMP_FINITE_CONVERSE |
![]() |
A | |
* | SIMP_FINITE_UPTO |
![]() |
A | |
* | SIMP_FINITE_ID |
![]() |
where ![]() ![]() |
A |
* | SIMP_FINITE_ID_DOMRES |
![]() |
A | |
* | SIMP_FINITE_PRJ1 |
![]() |
where ![]() ![]() |
A |
* | SIMP_FINITE_PRJ2 |
![]() |
where ![]() ![]() |
A |
* | SIMP_FINITE_PRJ1_DOMRES |
![]() |
A | |
* | SIMP_FINITE_PRJ2_DOMRES |
![]() |
A | |
* | SIMP_FINITE_NATURAL |
![]() |
A | |
* | SIMP_FINITE_NATURAL1 |
![]() |
A | |
* | SIMP_FINITE_INTEGER |
![]() |
A | |
* | SIMP_FINITE_BOOL |
![]() |
A | |
* | SIMP_FINITE_LAMBDA |
![]() |
where ![]() ![]() ![]() ![]() |
A |
* | SIMP_TYPE_IN |
![]() |
where ![]() |
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 ![]() |
A |
* | SIMP_MULTI_SUBSET |
![]() |
A | |
* | SIMP_EQUAL_CONSTR |
![]() |
where ![]() |
A |
* | SIMP_EQUAL_CONSTR_DIFF |
![]() |
where ![]() ![]() |
A |
* | SIMP_DESTR_CONSTR |
![]() |
where ![]() ![]() |
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_IN_MAPSTO |
![]() |
AM | |
* | DEF_IN_POW |
![]() |
M | |
* | DEF_IN_POW1 |
![]() |
M | |
* | DEF_SUBSETEQ |
![]() |
where ![]() ![]() ![]() |
M |
* | DEF_IN_BUNION |
![]() |
M | |
* | DEF_IN_BINTER |
![]() |
M | |
* | DEF_IN_SETMINUS |
![]() |
M | |
* | DEF_IN_SETENUM |
![]() |
M | |
* | DEF_IN_KUNION |
![]() |
where ![]() |
M |
* | DEF_IN_QUNION |
![]() |
where ![]() |
M |
* | DEF_IN_KINTER |
![]() |
where ![]() |
M |
* | DEF_IN_QINTER |
![]() |
where ![]() |
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 ![]() |
M |
* | DERIV_TYPE_SETMINUS_BUNION |
![]() |
where ![]() |
M |
* | DERIV_TYPE_SETMINUS_SETMINUS |
![]() |
where ![]() |
M |
DISTRI_CPROD_BINTER |
![]() |
M | ||
DISTRI_CPROD_BUNION |
![]() |
M | ||
DISTRI_CPROD_SETMINUS |
![]() |
M | ||
* | DERIV_SUBSETEQ |
![]() |
where ![]() ![]() ![]() |
M |
* | DERIV_EQUAL |
![]() |
where ![]() ![]() ![]() |
M |
* | DERIV_SUBSETEQ_SETMINUS_L |
![]() |
M | |
* | DERIV_SUBSETEQ_SETMINUS_R |
![]() |
M | |
* | DEF_PARTITION |
![]() |
AM | |
SIMP_EMPTY_PARTITION |
![]() |
A | ||
SIMP_SINGLE_PARTITION |
![]() |
A |