Difference between pages "Empty Set Rewrite Rules" and "CamilleX"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Josselin
(Fixed rule SIMP_STREL_EQUAL_EMPTY)
 
 
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
{{TOCright}}
Rules without a <tt>*</tt> are planned to be implemented in future versions.
+
Return to [[Rodin Plug-ins]]
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
 
  
{{RRHeader}}
+
The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
{{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
+
Extension to Event-B including the ''machine inclusion'' mechanism is also supported.
{{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_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_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_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  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 \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_EMPTY}}||<math>  i \upto j \;\;\defi\;\; i > j </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_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 \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_DOMSUB_EQUAL_EMPTY}}||<math> S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_RANRES_EQUAL_EMPTY}}||<math> r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset</math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_RANSUB_EQUAL_EMPTY}}||<math> r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_CONVERSE_EQUAL_EMPTY}}||<math> r^{-1} = \emptyset \;\;\defi\;\; 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 \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_PPROD_EQUAL_EMPTY}}||<math>  p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </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_PRJ2_EQUAL_EMPTY}}||<math>  \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 
|}
 
  
 +
<br style="clear: both" />
  
[[Category:User documentation|The Proving Perspective]]
+
Please have a look also at the [[CamilleX User Guide]].
[[Category:Rodin Platform|The Proving Perspective]]
+
 
[[Category:User manual|The Proving Perspective]]
+
=== Current version ===
 +
The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the ''CamilleX'' category).  Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.
 +
 
 +
=== Principles ===
 +
The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.

Latest revision as of 13:09, 19 July 2021

Return to Rodin Plug-ins

The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines. Extension to Event-B including the machine inclusion mechanism is also supported.


Please have a look also at the CamilleX User Guide.

Current version

The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the CamilleX category). Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.

Principles

The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.