Difference between revisions of "Empty Set Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Josselin (Fixed name rule SIMP_UPTO_EQUAL_INTEGER) |
imported>Josselin (Marked rules as implemented) |
||
(9 intermediate revisions by 2 users not shown) | |||
Line 3: | Line 3: | ||
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]]. | Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]]. | ||
− | All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math> and <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent. | + | All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math> and <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent. All rewrite rules that match the pattern <math>\textbf{P}=\mathit{Ty}</math> are also applicable to predicates of the form <math>\mathit{Ty}\subseteq\textbf{P}</math> and <math>\mathit{Ty}=\textbf{P}</math>, as these predicates are equivalent. |
{{RRHeader}} | {{RRHeader}} | ||
{{RRRow}}|*||{{Rulename|DEF_SPECIAL_NOT_EQUAL}}||<math> \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S </math>|| where <math>x</math> is not free in <math>S</math> || M | {{RRRow}}|*||{{Rulename|DEF_SPECIAL_NOT_EQUAL}}||<math> \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S </math>|| where <math>x</math> is not free in <math>S</math> || M | ||
− | {{RRRow}}|||{{Rulename|SIMP_SETENUM_EQUAL_EMPTY}}||<math> \{ A, \ldots , B\} = \emptyset \;\;\defi\;\; \bfalse </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_SETENUM_EQUAL_EMPTY}}||<math> \{ A, \ldots , B\} = \emptyset \;\;\defi\;\; \bfalse </math>|| || A |
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_COMPSET}}||<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>|| || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_COMPSET}}||<math> \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) </math>|| || A | ||
− | {{RRRow}}|||{{Rulename|SIMP_BINTER_EQUAL_TYPE}}||<math> A \binter \ | + | {{RRRow}}|*||{{Rulename|SIMP_BINTER_EQUAL_TYPE}}||<math> A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression || A |
− | {{RRRow}}|||{{Rulename|SIMP_BUNION_EQUAL_EMPTY}}||<math> A \bunion \ | + | {{RRRow}}|*||{{Rulename|SIMP_BINTER_SING_EQUAL_EMPTY}}||<math>A\binter\cdots\binter\{a\}\binter\cdots\binter B = \emptyset \;\;\defi\;\; \lnot\, a \in A\binter\cdots\binter B</math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_EMPTY}}||<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}||<math>A\binter\cdots\binter(B\setminus C)\binter\cdots\binter D = \emptyset \;\;\defi\;\; (A\binter\cdots\binter B\binter\cdots\binter D) \setminus C = \emptyset</math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_TYPE}}||<math> A \setminus B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land B = \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression || A | + | {{RRRow}}|*||{{Rulename|SIMP_BUNION_EQUAL_EMPTY}}||<math> A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_POW_EQUAL_EMPTY}}||<math> \pow (S) = \emptyset \;\;\defi\;\; \bfalse </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_SETMINUS_EQUAL_EMPTY}}||<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math> \pown (S) = \emptyset \;\;\defi\;\; S = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_SETMINUS_EQUAL_TYPE}}||<math> A \setminus B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land B = \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression || A |
− | {{RRRow}}|||{{Rulename|SIMP_KINTER_EQUAL_TYPE}}||<math> \inter (S) = \mathit{Ty} \;\;\defi\;\; S = \{ \mathit{Ty} \} </math>|| where <math>\mathit{Ty}</math> is a type expression || A | + | {{RRRow}}|*||{{Rulename|SIMP_POW_EQUAL_EMPTY}}||<math> \pow (S) = \emptyset \;\;\defi\;\; \bfalse </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_KUNION_EQUAL_EMPTY}}||<math> \union (S) = \emptyset \;\;\defi\;\; S \subseteq \{ \emptyset \} </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math> \pown (S) = \emptyset \;\;\defi\;\; S = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_QINTER_EQUAL_TYPE}}||<math> (\Inter x\qdot P(x) \mid E(x)) = \mathit{Ty} \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression || A | + | {{RRRow}}|*||{{Rulename|SIMP_KINTER_EQUAL_TYPE}}||<math> \inter (S) = \mathit{Ty} \;\;\defi\;\; S = \{ \mathit{Ty} \} </math>|| where <math>\mathit{Ty}</math> is a type expression || A |
− | {{RRRow}}|||{{Rulename|SIMP_QUNION_EQUAL_EMPTY}}||<math> (\Union x\qdot P(x) \mid E(x)) = \emptyset \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \emptyset</math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_KUNION_EQUAL_EMPTY}}||<math> \union (S) = \emptyset \;\;\defi\;\; S \subseteq \{ \emptyset \} </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_NATURAL_EQUAL_EMPTY}}||<math> \nat = \emptyset \;\;\defi\;\; \bfalse</math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_QINTER_EQUAL_TYPE}}||<math> (\Inter x\qdot P(x) \mid E(x)) = \mathit{Ty} \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression || A |
− | {{RRRow}}|||{{Rulename|SIMP_NATURAL1_EQUAL_EMPTY}}||<math> \natn = \emptyset \;\;\defi\;\; \bfalse</math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_QUNION_EQUAL_EMPTY}}||<math> (\Union x\qdot P(x) \mid E(x)) = \emptyset \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \emptyset</math>|| || A |
+ | {{RRRow}}|*||{{Rulename|SIMP_NATURAL_EQUAL_EMPTY}}||<math> \nat = \emptyset \;\;\defi\;\; \bfalse</math>|| || A | ||
+ | {{RRRow}}|*||{{Rulename|SIMP_NATURAL1_EQUAL_EMPTY}}||<math> \natn = \emptyset \;\;\defi\;\; \bfalse</math>|| || A | ||
{{RRRow}}|*||{{Rulename|SIMP_TYPE_EQUAL_EMPTY}}||<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression || A | {{RRRow}}|*||{{Rulename|SIMP_TYPE_EQUAL_EMPTY}}||<math> \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression || A | ||
− | {{RRRow}}|||{{Rulename|SIMP_CPROD_EQUAL_EMPTY}}||<math> S \cprod T = \emptyset \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_CPROD_EQUAL_EMPTY}}||<math> S \cprod T = \emptyset \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_CPROD_EQUAL_TYPE}}||<math> S \cprod T = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land T = \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | + | {{RRRow}}|*||{{Rulename|SIMP_CPROD_EQUAL_TYPE}}||<math> S \cprod T = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land T = \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A |
− | {{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_EMPTY}}||<math> i \upto j = \emptyset \;\;\defi\;\; i > j </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_UPTO_EQUAL_EMPTY}}||<math> i \upto j = \emptyset \;\;\defi\;\; i > j </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_INTEGER}}||<math> i \upto j = \intg \;\;\defi\;\; \bfalse </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_UPTO_EQUAL_INTEGER}}||<math> i \upto j = \intg \;\;\defi\;\; \bfalse </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_NATURAL}}||<math> i \upto j = \nat \;\;\defi\;\; \bfalse </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_UPTO_EQUAL_NATURAL}}||<math> i \upto j = \nat \;\;\defi\;\; \bfalse </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_NATURAL1}}||<math> i \upto j = \natn \;\;\defi\;\; \bfalse </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_UPTO_EQUAL_NATURAL1}}||<math> i \upto j = \natn \;\;\defi\;\; \bfalse </math>|| || A |
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_REL}}||<math> A \rel B = \emptyset \;\;\defi\;\; \bfalse </math>|| idem for operators <math>\pfun \pinj</math> || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_REL}}||<math> A \rel B = \emptyset \;\;\defi\;\; \bfalse </math>|| idem for operators <math>\pfun \pinj</math> || A | ||
{{RRRow}}|||{{Rulename|SIMP_TYPE_EQUAL_REL}}||<math> A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | {{RRRow}}|||{{Rulename|SIMP_TYPE_EQUAL_REL}}||<math> A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | ||
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOM}}||<math> A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset </math>|| idem for operator <math>\tfun</math> || A | {{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOM}}||<math> A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset </math>|| idem for operator <math>\tfun</math> || A | ||
− | {{RRRow}}|||{{Rulename| | + | {{RRRow}}|||{{Rulename|SIMP_TYPE_EQUAL_RELDOMRAN}}||<math> A \trel B = \mathit{Ty} \;\;\defi\;\; \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression, idem for operator <math>\srel, \strel, \tfun, \tinj, \psur, \tsur, \tbij</math> || A |
− | {{RRRow}}|||{{Rulename|SIMP_SREL_EQUAL_EMPTY}}||<math> A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_SREL_EQUAL_EMPTY}}||<math> A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_STREL_EQUAL_EMPTY}}||<math> A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_STREL_EQUAL_EMPTY}}||<math> A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_DOM_EQUAL_EMPTY}}||<math> \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_DOM_EQUAL_EMPTY}}||<math> \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_RAN_EQUAL_EMPTY}}||<math> \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_RAN_EQUAL_EMPTY}}||<math> \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_FCOMP_EQUAL_EMPTY}}||<math> p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_FCOMP_EQUAL_EMPTY}}||<math> p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_BCOMP_EQUAL_EMPTY}}||<math> p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_BCOMP_EQUAL_EMPTY}}||<math> p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_DOMRES_EQUAL_EMPTY}}||<math> S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_DOMRES_EQUAL_EMPTY}}||<math> S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_DOMRES_EQUAL_TYPE}}||<math> S \domres r = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land r = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | + | {{RRRow}}|*||{{Rulename|SIMP_DOMRES_EQUAL_TYPE}}||<math> S \domres r = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land r = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A |
− | {{RRRow}}|||{{Rulename|SIMP_DOMSUB_EQUAL_EMPTY}}||<math> S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_DOMSUB_EQUAL_EMPTY}}||<math> S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_DOMSUB_EQUAL_TYPE}}||<math> S \domsub r = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression || A | + | {{RRRow}}|*||{{Rulename|SIMP_DOMSUB_EQUAL_TYPE}}||<math> S \domsub r = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression || A |
− | {{RRRow}}|||{{Rulename|SIMP_RANRES_EQUAL_EMPTY}}||<math> r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset</math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_RANRES_EQUAL_EMPTY}}||<math> r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset</math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_RANRES_EQUAL_TYPE}}||<math> r \ranres S = \mathit{Ty} \;\;\defi\;\; S = \mathit{Tb} \land r = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A | + | {{RRRow}}|*||{{Rulename|SIMP_RANRES_EQUAL_TYPE}}||<math> r \ranres S = \mathit{Ty} \;\;\defi\;\; S = \mathit{Tb} \land r = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> || A |
− | {{RRRow}}|||{{Rulename|SIMP_RANSUB_EQUAL_EMPTY}}||<math> r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_RANSUB_EQUAL_EMPTY}}||<math> r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_RANSUB_EQUAL_TYPE}}||<math> r \ransub S = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression || A | + | {{RRRow}}|*||{{Rulename|SIMP_RANSUB_EQUAL_TYPE}}||<math> r \ransub S = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression || A |
− | {{RRRow}}|||{{Rulename|SIMP_CONVERSE_EQUAL_EMPTY}}||<math> r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset</math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_CONVERSE_EQUAL_EMPTY}}||<math> r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset</math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_CONVERSE_EQUAL_TYPE}}||<math> r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1}</math>|| where <math>\mathit{Ty}</math> is a type expression || A | + | {{RRRow}}|*||{{Rulename|SIMP_CONVERSE_EQUAL_TYPE}}||<math> r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1}</math>|| where <math>\mathit{Ty}</math> is a type expression || A |
− | {{RRRow}}|||{{Rulename|SIMP_RELIMAGE_EQUAL_EMPTY}}||<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_RELIMAGE_EQUAL_EMPTY}}||<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_OVERL_EQUAL_EMPTY}}||<math> r \ovl \ | + | {{RRRow}}|*||{{Rulename|SIMP_OVERL_EQUAL_EMPTY}}||<math> r \ovl \cdots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \cdots \land s = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_DPROD_EQUAL_EMPTY}}||<math> p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_DPROD_EQUAL_EMPTY}}||<math> p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_DPROD_EQUAL_TYPE}}||<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> || A | + | {{RRRow}}|*||{{Rulename|SIMP_DPROD_EQUAL_TYPE}}||<math> p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> || A |
− | {{RRRow}}|||{{Rulename|SIMP_PPROD_EQUAL_EMPTY}}||<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_PPROD_EQUAL_EMPTY}}||<math> p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_PPROD_EQUAL_TYPE}}||<math> p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{ | + | {{RRRow}}|*||{{Rulename|SIMP_PPROD_EQUAL_TYPE}}||<math> p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tc} \land q = \mathit{Tb} \cprod \mathit{Td} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>(\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td})</math> || A |
− | {{RRRow}}|||{{Rulename|SIMP_ID_EQUAL_EMPTY}}||<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_ID_EQUAL_EMPTY}}||<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>|| || A |
− | {{RRRow}}|||{{Rulename|SIMP_PRJ1_EQUAL_EMPTY}}||<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>|| || A | + | {{RRRow}}|*||{{Rulename|SIMP_PRJ1_EQUAL_EMPTY}}||<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>|| || A |
− | {{RRRow}}|||{{Rulename| | + | {{RRRow}}|*||{{Rulename|SIMP_PRJ2_EQUAL_EMPTY}}||<math> \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>|| || A |
− | |||
− | |||
|} | |} | ||
Latest revision as of 16:39, 12 May 2014
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.
All rewrite rules that match the pattern are also applicable to predicates of the form
and
, as these predicates are equivalent. All rewrite rules that match the pattern
are also applicable to predicates of the form
and
, as these predicates are equivalent.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | DEF_SPECIAL_NOT_EQUAL |
![]() |
where ![]() ![]() |
M |
* | SIMP_SETENUM_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_SPECIAL_EQUAL_COMPSET |
![]() |
A | |
* | SIMP_BINTER_EQUAL_TYPE |
![]() |
where ![]() |
A |
* | SIMP_BINTER_SING_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_BINTER_SETMINUS_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_BUNION_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_SETMINUS_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_SETMINUS_EQUAL_TYPE |
![]() |
where ![]() |
A |
* | SIMP_POW_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_POW1_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_KINTER_EQUAL_TYPE |
![]() |
where ![]() |
A |
* | SIMP_KUNION_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_QINTER_EQUAL_TYPE |
![]() |
where ![]() |
A |
* | SIMP_QUNION_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_NATURAL_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_NATURAL1_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_TYPE_EQUAL_EMPTY |
![]() |
where ![]() |
A |
* | SIMP_CPROD_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_CPROD_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A |
* | SIMP_UPTO_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_UPTO_EQUAL_INTEGER |
![]() |
A | |
* | SIMP_UPTO_EQUAL_NATURAL |
![]() |
A | |
* | SIMP_UPTO_EQUAL_NATURAL1 |
![]() |
A | |
* | SIMP_SPECIAL_EQUAL_REL |
![]() |
idem for operators ![]() |
A |
SIMP_TYPE_EQUAL_REL |
![]() |
where ![]() ![]() |
A | |
* | SIMP_SPECIAL_EQUAL_RELDOM |
![]() |
idem for operator ![]() |
A |
SIMP_TYPE_EQUAL_RELDOMRAN |
![]() |
where ![]() ![]() |
A | |
* | SIMP_SREL_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_STREL_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_DOM_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_RAN_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_FCOMP_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_BCOMP_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_DOMRES_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_DOMRES_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A |
* | SIMP_DOMSUB_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_DOMSUB_EQUAL_TYPE |
![]() |
where ![]() |
A |
* | SIMP_RANRES_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_RANRES_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A |
* | SIMP_RANSUB_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_RANSUB_EQUAL_TYPE |
![]() |
where ![]() |
A |
* | SIMP_CONVERSE_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_CONVERSE_EQUAL_TYPE |
![]() |
where ![]() |
A |
* | SIMP_RELIMAGE_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_OVERL_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_DPROD_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_DPROD_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A |
* | SIMP_PPROD_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_PPROD_EQUAL_TYPE |
![]() |
where ![]() ![]() |
A |
* | SIMP_ID_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_PRJ1_EQUAL_EMPTY |
![]() |
A | |
* | SIMP_PRJ2_EQUAL_EMPTY |
![]() |
A |