Difference between revisions of "Empty Set Rewrite Rules"
From Event-B
Jump to navigationJump to searchimported>Josselin (Added rules EQUAL_EMPTY) |
imported>Josselin (Removed rule SIMP_BINTER_EQUAL_EMPTY and fixed rule SIMP_QUNION_EQUAL_EMPTY) |
||
Line 7: | Line 7: | ||
{{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_BUNION_EQUAL_EMPTY}}||<math> A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \ldots \land B = \emptyset </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_BUNION_EQUAL_EMPTY}}||<math> A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \ldots \land B = \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_EMPTY}}||<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_EMPTY}}||<math> A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B </math>|| || A | ||
Line 13: | Line 12: | ||
{{RRRow}}|||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math> \pown (S) = \emptyset \;\;\defi\;\; S = \emptyset </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math> \pown (S) = \emptyset \;\;\defi\;\; S = \emptyset </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_KUNION_EQUAL_EMPTY}}||<math> \union (S) = \emptyset \;\;\defi\;\; S \subseteq \{ \emptyset \} </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_KUNION_EQUAL_EMPTY}}||<math> \union (S) = \emptyset \;\;\defi\;\; S \subseteq \{ \emptyset \} </math>|| || A | ||
− | {{RRRow}}|||{{Rulename|SIMP_QUNION_EQUAL_EMPTY}}||<math> (\Union x\qdot P(x) \mid | + | {{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_BOOL_EQUAL_EMPTY}}||<math> \Bool = \emptyset \;\;\defi\;\; \bfalse</math>|| || A | {{RRRow}}|||{{Rulename|SIMP_BOOL_EQUAL_EMPTY}}||<math> \Bool = \emptyset \;\;\defi\;\; \bfalse</math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_INT_EQUAL_EMPTY}}||<math> \intg = \emptyset \;\;\defi\;\; \bfalse</math>|| || A | {{RRRow}}|||{{Rulename|SIMP_INT_EQUAL_EMPTY}}||<math> \intg = \emptyset \;\;\defi\;\; \bfalse</math>|| || A |
Revision as of 07:31, 30 April 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 | |
---|---|---|---|---|
* | DEF_SPECIAL_NOT_EQUAL |
![]() |
where ![]() ![]() |
M |
SIMP_SETENUM_EQUAL_EMPTY |
![]() |
A | ||
* | SIMP_SPECIAL_EQUAL_COMPSET |
![]() |
A | |
SIMP_BUNION_EQUAL_EMPTY |
![]() |
A | ||
SIMP_SETMINUS_EQUAL_EMPTY |
![]() |
A | ||
SIMP_POW_EQUAL_EMPTY |
![]() |
A | ||
SIMP_POW1_EQUAL_EMPTY |
![]() |
A | ||
SIMP_KUNION_EQUAL_EMPTY |
![]() |
A | ||
SIMP_QUNION_EQUAL_EMPTY |
![]() |
A | ||
SIMP_BOOL_EQUAL_EMPTY |
![]() |
A | ||
SIMP_INT_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_UPTO_EQUAL_EMPTY |
![]() |
where ![]() ![]() |
A | |
* | SIMP_SPECIAL_EQUAL_REL |
![]() |
idem for operators ![]() |
A |
* | SIMP_SPECIAL_EQUAL_RELDOM |
![]() |
idem for operator ![]() |
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_DOMSUB_EQUAL_EMPTY |
![]() |
A | ||
SIMP_RANRES_EQUAL_EMPTY |
![]() |
A | ||
SIMP_RANSUB_EQUAL_EMPTY |
![]() |
A | ||
SIMP_CONVERSE_EQUAL_EMPTY |
![]() |
A | ||
SIMP_RELIMAGE_EQUAL_EMPTY |
![]() |
A | ||
SIMP_OVERL_EQUAL_EMPTY |
![]() |
A | ||
SIMP_DPROD_EQUAL_EMPTY |
![]() |
A | ||
SIMP_PPROD_EQUAL_EMPTY |
![]() |
A | ||
SIMP_ID_EQUAL_EMPTY |
![]() |
A | ||
SIMP_PRJ1_EQUAL_EMPTY |
![]() |
A | ||
SIMP_PRJ2_EQUAL_EMPTY |
![]() |
A |