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

@@ 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]].
-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.
+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.
-{{RRHeader}}
+<br style="clear: both" />
-{{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
-|}
+Please have a look also at the [[CamilleX User Guide]].
-[[Category:User documentation|The Proving Perspective]]
+=== Current version ===
-[[Category:Rodin Platform|The Proving Perspective]]
+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.
-[[Category:User manual|The Proving Perspective]]
+=== 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.

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

Latest revision as of 13:09, 19 July 2021

Contents

Current version

Principles

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools