Difference between pages "Empty Set Rewrite Rules" and "Event-B Modelling Language"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Josselin
(Fixed name rule SIMP_UPTO_EQUAL_INTEGER)
 
imported>Ladenberger
 
Line 1: Line 1:
−
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
This page gives a brief summary of documents describing Event-B's modeling notation.  
−
Rules without a <tt>*</tt> are planned to be implemented in future versions.
 
−
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.
+
=Rodin Handbook=
  
−
{{RRHeader}}
+
[http://handbook.event-b.org/current/html/modeling_notation.html Rodin Handbook (Modeling Notation)]
−
{{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_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 \ldots \binter B = \mathit{Ty} \;\;\defi\;\;  A = \mathit{Ty} \land \ldots \land B  = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  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_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_POW_EQUAL_EMPTY}}||<math>  \pow (S) = \emptyset \;\;\defi\;\;  \bfalse  </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math>  \pown (S) = \emptyset \;\;\defi\;\;  S = \emptyset  </math>||  ||  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_KUNION_EQUAL_EMPTY}}||<math>  \union (S) = \emptyset \;\;\defi\;\;  S \subseteq \{ \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_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_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_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_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_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_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_TYPE_EQUAL_RELDOM}}||<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, \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_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_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_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_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_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_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_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_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_OVERL_EQUAL_EMPTY}}||<math>  r \ovl \ldots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \ldots \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_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_TYPE}}||<math>  p \pprod q = \mathit{Ty} \;\;\defi\;\;  p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Tc} \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_PRJ1_EQUAL_EMPTY}}||<math>  \prjone = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_PRJ1_EQUAL_TYPE}}||<math>  \prjone = \mathit{Ty} \;\;\defi\;\; \finite(\mathit{Ta}) \land \card(\mathit{Ta})=1 </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb} \cprod \mathit{Ta}</math> ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_PRJ2_EQUAL_EMPTY}}||<math>  \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 
−
{{RRRow}}|||{{Rulename|SIMP_PRJ2_EQUAL_TYPE}}||<math>  \prjtwo = \mathit{Ty} \;\;\defi\;\; \finite(\mathit{Tb}) \land \card(\mathit{Tb})=1 </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb} \cprod \mathit{Tb}</math> ||  A
 
−
|}
 
  
 +
<small>
 +
The original and now outdated version is available [http://deploy-eprints.ecs.soton.ac.uk/11/3/notation-1.5.pdf in PDF format here].
 +
</small>
  
−
[[Category:User documentation|The Proving Perspective]]
+
[[Category:User documentation]]
−
[[Category:Rodin Platform|The Proving Perspective]]
+
[[Category:Event-B]]
−
[[Category:User manual|The Proving Perspective]]
 

Latest revision as of 08:45, 27 October 2011

This page gives a brief summary of documents describing Event-B's modeling notation.

Rodin Handbook

Rodin Handbook (Modeling Notation)

The original and now outdated version is available in PDF format here.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Empty_Set_Rewrite_Rules&oldid=4188’