Empty Set Rewrite Rules

From Event-B
Revision as of 07:31, 30 April 2013 by imported>Josselin (Removed rule SIMP_BINTER_EQUAL_EMPTY and fixed rule SIMP_QUNION_EQUAL_EMPTY)
Jump to navigationJump to search

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_BOOL_EQUAL_EMPTY
  \Bool = \emptyset \;\;\defi\;\;  \bfalse A
SIMP_INT_EQUAL_EMPTY
  \intg = \emptyset \;\;\defi\;\;  \bfalse 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 where i and j are literals 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 \rel 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 (p) \binter \dom (q) = \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