Difference between revisions of "Empty Set Rewrite Rules"

From Event-B
Jump to navigationJump to search
imported>Josselin
(Fixed rule SIMP_UPTO_EQUAL_EMPTY (removed side condition))
imported>Josselin
(Fixed rule SIMP_BCOMP_EQUAL_EMPTY)
(One intermediate revision by the same user not shown)
Line 20: Line 20:
 
{{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_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|SIMP_SREL_EQUAL_EMPTY}}||<math>  A \rel B \;\;\defi\;\; A = \emptyset \land  \lnot\,B = \emptyset </math>||  ||  A
+
{{RRRow}}|||{{Rulename|SIMP_SREL_EQUAL_EMPTY}}||<math>  A \srel B \;\;\defi\;\; A = \emptyset \land  \lnot\,B = \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_STREL_EQUAL_EMPTY}}||<math>  A \strel B \;\;\defi\;\; (A = \emptyset \;\;\defi\;\;  \lnot\,B = \emptyset) </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_STREL_EQUAL_EMPTY}}||<math>  A \strel B \;\;\defi\;\; (A = \emptyset \;\;\defi\;\;  \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 (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_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_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

Revision as of 08:07, 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
  \lnot\, S = \emptyset  \;\;\defi\;\;  \exists x \qdot  x \in  S where x is not free in S M
SIMP_SETENUM_EQUAL_EMPTY
  \{ A, \ldots , B\}  = \emptyset \;\;\defi\;\;  \bfalse A
*
SIMP_SPECIAL_EQUAL_COMPSET
  \{  x \qdot  P(x) \mid  E \}  = \emptyset  \;\;\defi\;\;  \forall x\qdot  \lnot\, P(x) A
SIMP_BUNION_EQUAL_EMPTY
  A \bunion \ldots \bunion B = \emptyset \;\;\defi\;\;  A = \emptyset \land \ldots \land B  = \emptyset A
SIMP_SETMINUS_EQUAL_EMPTY
  A \setminus  B = \emptyset \;\;\defi\;\;  A \subseteq  B  A
SIMP_POW_EQUAL_EMPTY
  \pow (S) = \emptyset \;\;\defi\;\;  \bfalse  A
SIMP_POW1_EQUAL_EMPTY
  \pown (S) = \emptyset \;\;\defi\;\;  S = \emptyset  A
SIMP_KUNION_EQUAL_EMPTY
   \union (S) = \emptyset \;\;\defi\;\;  S \subseteq \{ \emptyset \}  A
SIMP_QUNION_EQUAL_EMPTY
  (\Union  x\qdot P(x)  \mid  E(x)) = \emptyset \;\;\defi\;\;  \forall x\qdot  P(x) \limp E(x) = \emptyset A
SIMP_NATURAL_EQUAL_EMPTY
  \nat = \emptyset \;\;\defi\;\;  \bfalse A
SIMP_NATURAL1_EQUAL_EMPTY
  \natn = \emptyset \;\;\defi\;\;  \bfalse A
*
SIMP_TYPE_EQUAL_EMPTY
 \mathit{Ty} = \emptyset  \;\;\defi\;\;  \bfalse where \mathit{Ty} is a type expression A
SIMP_CPROD_EQUAL_EMPTY
  S \cprod T \;\;\defi\;\; S = \emptyset \lor T = \emptyset A
SIMP_UPTO_EQUAL_EMPTY
  i \upto j \;\;\defi\;\; i > j A
*
SIMP_SPECIAL_EQUAL_REL
  A \rel  B = \emptyset  \;\;\defi\;\;  \bfalse idem for operators \pfun  \pinj A
*
SIMP_SPECIAL_EQUAL_RELDOM
  A \trel  B = \emptyset  \;\;\defi\;\;  \lnot\, A = \emptyset  \land  B = \emptyset idem for operator \tfun A
SIMP_SREL_EQUAL_EMPTY
  A \srel B \;\;\defi\;\; A = \emptyset \land  \lnot\,B = \emptyset A
SIMP_STREL_EQUAL_EMPTY
  A \strel B \;\;\defi\;\; (A = \emptyset \;\;\defi\;\;  \lnot\,B = \emptyset) A
SIMP_DOM_EQUAL_EMPTY
  \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset  A
SIMP_RAN_EQUAL_EMPTY
  \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset  A
SIMP_FCOMP_EQUAL_EMPTY
 p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset  A
SIMP_BCOMP_EQUAL_EMPTY
 p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset  A
SIMP_DOMRES_EQUAL_EMPTY
 S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset  A
SIMP_DOMSUB_EQUAL_EMPTY
 S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S A
SIMP_RANRES_EQUAL_EMPTY
 r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset A
SIMP_RANSUB_EQUAL_EMPTY
 r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S A
SIMP_CONVERSE_EQUAL_EMPTY
 r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset A
SIMP_RELIMAGE_EQUAL_EMPTY
 r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset A
SIMP_OVERL_EQUAL_EMPTY
  r \ovl \ldots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \ldots \land s =  \emptyset A
SIMP_DPROD_EQUAL_EMPTY
  p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset A
SIMP_PPROD_EQUAL_EMPTY
  p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset A
SIMP_ID_EQUAL_EMPTY
  \id = \emptyset \;\;\defi\;\; \bfalse A
SIMP_PRJ1_EQUAL_EMPTY
  \prjone = \emptyset \;\;\defi\;\; \bfalse A
SIMP_PRJ2_EQUAL_EMPTY
  \prjtwo = \emptyset \;\;\defi\;\; \bfalse A