Difference between pages "Plug-in Tutorial" and "Relation Rewrite Rules"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Nicolas
m (updated rule SIMP_DOMRES_ID to math V2)
 
Line 1: Line 1:
−
{{Navigation|Next= [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]]}}
+
{{RRHeader}}
 +
{{RRRow}}|*||{{Rulename|SIMP_DOM_COMPSET}}||<math>  \dom (\{ x \mapsto  a, \ldots , y \mapsto  b\} ) \;\;\defi\;\;  \{ x, \ldots , y\} </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_DOM_CONVERSE}}||<math>  \dom (r^{-1} ) \;\;\defi\;\;  \ran (r) </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RAN_COMPSET}}||<math>  \ran (\{ x \mapsto  a, \ldots , y \mapsto  b\} ) \;\;\defi\;\;  \{ a, \ldots , b\} </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RAN_CONVERSE}}||<math>  \ran (r^{-1} ) \;\;\defi\;\;  \dom (r) </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OVERL}}||<math>  r \ovl  \ldots  \ovl  \emptyset  \ovl  \ldots  \ovl  s \;\;\defi\;\;  r \ovl  \ldots  \ovl  s </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_OVERL}}||<math>\begin{array}{cl} & r \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \\ \defi &  r \ovl  \ldots  \ovl  \ldots  \ovl  s \ovl  \ldots  \ovl  u \end{array}</math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_OVERL_CPROD}}||<math>  r \ovl  (\mathit{Ty} \cprod  S) \;\;\defi\;\;  (\mathit{Ty} \cprod  S) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMRES_L}}||<math>  \emptyset  \domres  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMRES_R}}||<math>  S \domres  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DOMRES}}||<math> \mathit{Ty} \domres  r \;\;\defi\;\;  r </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMRES_DOM}}||<math>  \dom (r) \domres  r \;\;\defi\;\;  r </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMRES_RAN}}||<math>  \ran (r) \domres  r^{-1}  \;\;\defi\;\;  r^{-1} </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_DOMRES_ID}}||<math>  S \domres  (T \domres \id) \;\;\defi\;\;  (S \binter  T) \domres \id </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANRES_R}}||<math>  r \ranres  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANRES_L}}||<math>  \emptyset  \ranres  S \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RANRES}}||<math>  r \ranres  \mathit{Ty} \;\;\defi\;\;  r </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RANRES_RAN}}||<math>  r \ranres  \ran (r) \;\;\defi\;\;  r </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RANRES_DOM}}||<math>  r^{-1}  \ranres  \dom (r) \;\;\defi\;\;  r^{-1} </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RANRES_ID}}||<math>  (S \domres \id) \ranres  T \;\;\defi\;\;  (S \binter  T) \domres \id </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMSUB_L}}||<math>  \emptyset  \domsub  r \;\;\defi\;\;  r </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DOMSUB_R}}||<math>  S \domsub  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DOMSUB}}||<math> \mathit{Ty} \domsub  r \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOMSUB_DOM}}||<math>  \dom (r) \domsub  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_DOMSUB_ID}}||<math>  S \domsub  \id (T) \;\;\defi\;\;  \id (T \setminus S) </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANSUB_R}}||<math>  r \ransub  \emptyset  \;\;\defi\;\;  r </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RANSUB_L}}||<math>  \emptyset  \ransub  S \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RANSUB}}||<math>  r \ransub  \mathit{Ty} \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RANSUB_RAN}}||<math>  r \ransub  \ran (r) \;\;\defi\;\;  \emptyset </math>||  || A
 +
{{RRRow}}|*||{{Rulename|SIMP_RANSUB_ID}}||<math>  (S \domres \id) \ransub  T \;\;\defi\;\;  (S \setminus T) \domres \id </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_FCOMP}}||<math>  r \fcomp \ldots  \fcomp \emptyset  \fcomp \ldots  \fcomp s \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_FCOMP_ID}}||<math>  r \fcomp \ldots  \fcomp \id \fcomp \ldots  \fcomp s \;\;\defi\;\;  r \fcomp \ldots  \fcomp s </math>|| ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_FCOMP_R}}||<math>  r \fcomp \mathit{Ty} \;\;\defi\;\;  \dom (r) \cprod  \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_TYPE_FCOMP_L}}||<math> \mathit{Ty} \fcomp r \;\;\defi\;\;  \mathit{Ta} \cprod  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID}}||<math>  r \fcomp \ldots  \fcomp S \domres \id \fcomp T \domres \id \fcomp \ldots  s \;\;\defi\;\;  r \fcomp \ldots  \fcomp (S \binter  T) \domres \id \fcomp \ldots  \fcomp s </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_BCOMP}}||<math>  r \bcomp  \ldots  \bcomp  \emptyset  \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BCOMP_ID}}||<math>  r \bcomp  \ldots  \bcomp  \id \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  r \bcomp  \ldots  \bcomp  s </math>|| ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BCOMP_L}}||<math> \mathit{Ty} \bcomp  r \;\;\defi\;\;  \dom (r) \cprod  \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_TYPE_BCOMP_R}}||<math>  r \bcomp  \mathit{Ty} \;\;\defi\;\;  \mathit{Ta} \cprod  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_BCOMP_ID}}||<math>  r \bcomp  \ldots  \bcomp S \domres \id \bcomp T \domres \id \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  r \bcomp  \ldots  \bcomp (S \binter  T) \domres \id \bcomp  \ldots  \bcomp  s </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DPROD_R}}||<math>  r \dprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_DPROD_L}}||<math>  \emptyset  \dprod  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DPROD}}||<math> \mathit{Ta} \dprod  \mathit{Tb} \;\;\defi\;\;  Tc \cprod  (Td \cprod  Te) </math>|| where <math>\mathit{Ta}</math> and <math>\mathit{Tb}</math> are type expressions and <math>\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}</math> and <math>\mathit{Tb} = \mathit{Tc} \cprod \mathit{Te}</math> ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PPROD_R}}||<math>  r \pprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PPROD_L}}||<math>  \emptyset  \pprod  r \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_PPROD}}||<math> \mathit{Ta} \pprod  \mathit{Tb} \;\;\defi\;\;  (Tc \cprod  Te) \cprod  (Td \cprod  Tf) </math>|| where <math>\mathit{Ta}</math> and <math>\mathit{Tb}</math> are type expressions and <math>\mathit{Ta} = \mathit{Tc} \cprod \mathit{Td}</math> and <math>\mathit{Tb} = \mathit{Te} \cprod \mathit{Tf}</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RELIMAGE_R}}||<math>  r[\emptyset ] \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_RELIMAGE_L}}||<math>  \emptyset [S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RELIMAGE}}||<math>  r[Ty] \;\;\defi\;\;  \ran (r) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_DOM}}||<math>  r[\dom (r)] \;\;\defi\;\;  \ran (r) </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RELIMAGE_ID}}||<math>  \id[T] \;\;\defi\;\;  T </math>|| ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RELIMAGE_ID}}||<math>  (S \domres \id)[T] \;\;\defi\;\;  S \binter  T </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_CPROD_SING}}||<math>  (\{ E\}  \cprod  S)[\{ E\} ] \;\;\defi\;\;  S </math>|| where <math>E</math> is a single expression ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_SING_MAPSTO}}||<math>  \{ E \mapsto  F\} [\{ E\} ] \;\;\defi\;\;  \{ F\} </math>|| where <math>E</math> is a single expression ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB}}||<math>  (r \ransub  S)^{-1} [S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_CONVERSE_RANRES}}||<math>  (r \ranres  S)^{-1} [S] \;\;\defi\;\;  r^{-1} [S] </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RELIMAGE_CONVERSE_DOMSUB}}||<math>  (S \domsub  r)^{-1} [T] \;\;\defi\;\;  r^{-1} [T] \setminus S </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_RANSUB}}||<math>  (r \ransub  S)[T] \;\;\defi\;\;  r[T] \setminus S </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_RANRES}}||<math>  (r \ranres  S)[T] \;\;\defi\;\;  r[T] \binter  S </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RELIMAGE_DOMSUB}}||<math>  (S \domsub  r)[S] \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_DOMSUB}}||<math>  (S \domsub  r)[T] \;\;\defi\;\;  r[T \setminus S] </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_DOMRES}}||<math>  (S \domres  r)[T] \;\;\defi\;\;  r[S \binter  T] </math>||  ||  M
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_CONVERSE}}||<math>  \emptyset ^{-1}  \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_ID}}||<math>  \id^{-1}  \;\;\defi\;\;  \id </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_CONVERSE}}||<math> \mathit{Ty}^{-1}  \;\;\defi\;\;  \mathit{Tb} \cprod  \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_SETENUM}}||<math>  \{ x \mapsto  a, \ldots , y \mapsto  b\} ^{-1}  \;\;\defi\;\;  \{ a \mapsto  x, \ldots , b \mapsto  y\} </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_COMPSET}}||<math>  \{ x, \ldots , y \qdot  P \mid  x, \ldots , y\} ^{-1}  \;\;\defi\;\;  \{ y, \ldots , x \qdot  P \mid  y, \ldots , x\} </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_ID}}||<math> \emptyset \domres \id \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_DOM_ID}}||<math>  \dom (\id) \;\;\defi\;\;  S </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RAN_ID}}||<math>  \ran (\id) \;\;\defi\;\;  S </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID_L}}||<math>  (S \domres \id) \fcomp r \;\;\defi\;\;  S \domres  r </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FCOMP_ID_R}}||<math>  r \fcomp (S \domres \id) \;\;\defi\;\;  r \ranres  S </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_REL_R}}||<math>  S \rel  \emptyset  \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\srel  \pfun  \pinj  \psur</math> ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_REL_L}}||<math>  \emptyset  \rel  S \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\trel  \pfun  \tfun  \pinj  \tinj</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 operators <math>\tfun  \tinj  \tsur  \tbij</math> ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PRJ1}}||<math>  \emptyset \domres \prjone \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_PRJ2}}||<math>  \emptyset \domres \prjtwo \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_PRJ1}}||<math>  \prjone (E \mapsto  F) \;\;\defi\;\;  E </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_PRJ2}}||<math>  \prjtwo (E \mapsto  F) \;\;\defi\;\;  F </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_DOM_PRJ1}}||<math>  \dom (\prjone) \;\;\defi\;\;  S \cprod T </math>|| where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_DOM_PRJ2}}||<math>  \dom (\prjtwo) \;\;\defi\;\; S \cprod T </math>|| where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RAN_PRJ1}}||<math>  \ran (\prjone) \;\;\defi\;\;  S </math>|| where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RAN_PRJ2}}||<math>  \ran (\prjtwo) \;\;\defi\;\;  T </math>|| where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> ||  A
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_LAMBDA}}||<math>  (\lambda x \qdot  \bfalse  \mid  E) \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_LAMBDA}}||<math>  (\lambda x \qdot  P(x) \mid  E(x))(y) \;\;\defi\;\;  E(y) </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_DOM_LAMBDA}}||<math>  \dom (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \{ x\qdot  P \mid  x\} </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_RAN_LAMBDA}}||<math>  \ran (\lambda x \qdot  P \mid  E) \;\;\defi\;\;  \{ x\qdot  P \mid  E\} </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_SETENUM_LL}}||<math>  \{ A \mapsto  E, \ldots  , B \mapsto  E\} (x) \;\;\defi\;\;  E </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_SETENUM_LR}}||<math>  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} (x) \;\;\defi\;\;  y </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_OVERL_SETENUM}}||<math>  (r \ovl  \ldots  \ovl  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} )(x) \;\;\defi\;\;  y </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_FUNIMAGE_BUNION_SETENUM}}||<math>  (r \bunion  \ldots  \bunion  \{ A \mapsto  E, \ldots  , x \mapsto  y, \ldots  , B \mapsto  F\} )(x) \;\;\defi\;\;  y </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_CPROD}}||<math>  (S \cprod  \{ F\} )(x) \;\;\defi\;\;  F </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_ID}}||<math>  \id (x) \;\;\defi\;\;  x </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_FUNIMAGE_CONVERSE}}||<math>  f(f^{-1} (E)) \;\;\defi\;\;  E </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_CONVERSE_FUNIMAGE}}||<math>  f^{-1}(f(E)) \;\;\defi\;\;  E </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM}}||<math>  \{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\;  E </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|DEF_BCOMP}}||<math>  r \bcomp  \ldots  \bcomp  s \;\;\defi\;\;  s \fcomp \ldots  \fcomp r </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_ID_SING}}||<math>  \{ E\} \domres \id \;\;\defi\;\;  \{ E \mapsto  E\} </math>|| where <math>E</math> is a single expression ||  M
 +
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_DOM}}||<math>  \dom (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_RAN}}||<math>  \ran (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_CONVERSE_CONVERSE}}||<math>  r^{-1-1}  \;\;\defi\;\;  r </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|DERIV_RELIMAGE_FCOMP}}||<math>  (p \fcomp q)[s] \;\;\defi\;\;  q[p[s]] </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_DOMRES}}||<math>  (s \domres  p) \fcomp q \;\;\defi\;\;  s \domres  (p \fcomp q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_DOMSUB}}||<math>  (s \domsub  p) \fcomp q \;\;\defi\;\;  s \domsub  (p \fcomp q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_RANRES}}||<math>  p \fcomp (q \ranres  s) \;\;\defi\;\;  (p \fcomp q) \ranres  s </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_FCOMP_RANSUB}}||<math>  p \fcomp (q \ransub  s) \;\;\defi\;\;  (p \fcomp q) \ransub  s </math>||  ||  M
 +
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOMRAN}}||<math>  \emptyset  \strel  \emptyset  \;\;\defi\;\;  \{ \emptyset \} </math>|| idem for operators <math>\tsur  \tbij</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_DOM}}||<math>  \dom (\mathit{Ty}) \;\;\defi\;\;  \mathit{Ta} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \rel \mathit{Tb}</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_RAN}}||<math>  \ran (\mathit{Ty}) \;\;\defi\;\;  \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \rel \mathit{Tb}</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOM_CPROD}}||<math>  \dom (E \cprod  E) \;\;\defi\;\;  E </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_RAN_CPROD}}||<math>  \ran (E \cprod  E) \;\;\defi\;\;  E </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|DEF_IN_DOM}}||<math>  E \in  \dom (r) \;\;\defi\;\;  \exists y \qdot  E \mapsto  y \in  r </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_RAN}}||<math>  F \in  \ran (r) \;\;\defi\;\;  \exists x \qdot  x \mapsto  F  \in  r </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_CONVERSE}}||<math>  E \mapsto  F \in  r^{-1}  \;\;\defi\;\;  F \mapsto  E \in  r </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_DOMRES}}||<math>  E \mapsto  F \in  S \domres  r \;\;\defi\;\;  E \in  S \land  E \mapsto  F \in  r </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_RANRES}}||<math>  E \mapsto  F \in  r \ranres  T \;\;\defi\;\;  E \mapsto  F \in  r \land  F \in  T </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_DOMSUB}}||<math>  E \mapsto  F \in  S \domsub  r \;\;\defi\;\;  E \notin  S \land  E \mapsto  F \in  r </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_RANSUB}}||<math>  E \mapsto  F \in  r \ranres  T \;\;\defi\;\;  E \mapsto  F \in  r \land  F \notin  T </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_RELIMAGE}}||<math>  F \in  r[w] \;\;\defi\;\;  \exists x \qdot  x \in  w \land  x \mapsto  F \in  r </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_FCOMP}}||<math>  E \mapsto  F \in  (p \fcomp q) \;\;\defi\;\;  \exists x \qdot  E \mapsto  x \in  p \land  x \mapsto  F \in  q </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_OVERL}}||<math>  p \ovl  q \;\;\defi\;\;  (\dom (q) \domsub  p) \bunion  q </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_ID}}||<math>  E \mapsto  F \in  \id \;\;\defi\;\;  E = F </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_DPROD}}||<math>  E \mapsto  (F \mapsto  G) \in  p \dprod  q \;\;\defi\;\;  E \mapsto  F \in  p \land  E \mapsto  G \in  q </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_PPROD}}||<math>  (E \mapsto  G) \mapsto  (F \mapsto  H) \in  p \pprod  q \;\;\defi\;\;  E \mapsto  F \in  p \land  G \mapsto  H \in  q </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_RELDOM}}||<math>  r \in  S \trel  T \;\;\defi\;\;  r \in  S \rel  T \land  \dom (r) = S </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_RELRAN}}||<math>  r \in  S \trel  T \;\;\defi\;\;  r \in  S \rel  T \land  \ran (r) = T </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_RELDOMRAN}}||<math>  r \in  S \strel  T \;\;\defi\;\;  r \in  S \rel  T \land  \dom (r) = S \land  \ran (r) = T </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_FCT}}||<math>\begin{array}{rcl}
 +
f \in  S \pfun  T & \defi & f \in  S \rel  T  \\  & \land & (\forall x,y,z \qdot  x \mapsto  y \in  f \land  x \mapsto  z \in  f \limp  y = z) \\ \end{array} </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_TFCT}}||<math>  f \in  S \tfun  T \;\;\defi\;\;  f \in  S \pfun  T \land  \dom (f) = S </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_INJ}}||<math>  f \in  S \pinj  T \;\;\defi\;\;  f \in  S \pfun  T \land  f^{-1}  \in  T \pfun  S </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_TINJ}}||<math>  f \in  S \tinj  T \;\;\defi\;\;  f \in  S \pinj  T \land  \dom (f) = S </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_SURJ}}||<math>  f \in  S \pfun  T \;\;\defi\;\;  f \in  S \pfun  T \land  \ran (f) = T </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_TSURJ}}||<math>  f \in  S \tsur  T \;\;\defi\;\;  f \in  S \psur  T \land  \dom (f) = S </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DEF_IN_BIJ}}||<math>  f \in  S \tbij  T \;\;\defi\;\;  f \in  S \tinj  T \land  \ran (f) = T </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_BCOMP_BUNION}}||<math>  r \bcomp  (s \bunion  t) \;\;\defi\;\;  (r \bcomp  s) \bunion  (r \bcomp  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_FCOMP_BUNION_R}}||<math>  p \fcomp (q \bunion  r) \;\;\defi\;\;  (p \fcomp q) \bunion  (p \fcomp r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_FCOMP_BUNION_L}}||<math>  (q \bunion  r) \fcomp p \;\;\defi\;\;  (q \fcomp p) \bunion  (r \fcomp p) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_BUNION}}||<math>  r \dprod  (s \bunion  t) \;\;\defi\;\;  (r \dprod  s) \bunion  (r \dprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_BINTER}}||<math>  r \dprod  (s \binter  t) \;\;\defi\;\;  (r \dprod  s) \binter  (r \dprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_SETMINUS}}||<math>  r \dprod  (s \setminus t) \;\;\defi\;\;  (r \dprod  s) \setminus (r \dprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DPROD_OVERL}}||<math>  r \dprod  (s \ovl  t) \;\;\defi\;\;  (r \dprod  s) \ovl  (r \dprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_BUNION}}||<math>  r \pprod  (s \bunion  t) \;\;\defi\;\;  (r \pprod  s) \bunion  (r \pprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_BINTER}}||<math>  r \pprod  (s \binter  t) \;\;\defi\;\;  (r \pprod  s) \binter  (r \pprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_SETMINUS}}||<math>  r \pprod  (s \setminus t) \;\;\defi\;\;  (r \pprod  s) \setminus (r \pprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_PPROD_OVERL}}||<math>  r \pprod  (s \ovl  t) \;\;\defi\;\;  (r \pprod  s) \ovl  (r \pprod  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_OVERL_BUNION_L}}||<math>  (p \bunion  q) \ovl  r \;\;\defi\;\;  (p \ovl  r) \bunion  (q \ovl  r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_OVERL_BINTER_L}}||<math>  (p \binter  q) \ovl  r \;\;\defi\;\;  (p \ovl  r) \binter  (q \ovl  r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BUNION_R}}||<math>  s \domres  (p \bunion  q) \;\;\defi\;\;  (s \domres  p) \bunion  (s \domres  q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BUNION_L}}||<math>  (s \bunion  t) \domres  r \;\;\defi\;\;  (s \domres  r) \bunion  (t \domres  r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BINTER_R}}||<math>  s \domres  (p \binter  q) \;\;\defi\;\;  (s \domres  p) \binter  (s \domres  q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_BINTER_L}}||<math>  (s \binter  t) \domres  r \;\;\defi\;\;  (s \domres  r) \binter  (t \domres  r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_SETMINUS_R}}||<math>  s \domres  (p \setminus q) \;\;\defi\;\;  (s \domres  p) \setminus (s \domres  q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_SETMINUS_L}}||<math>  (s \setminus t) \domres  r \;\;\defi\;\;  (s \domres  r) \setminus (t \domres  r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_DPROD}}||<math>  s \domres  (p \dprod  q) \;\;\defi\;\;  (s \domres  p) \dprod  (s \domres  q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMRES_OVERL}}||<math>  s \domres  (r \ovl  q) \;\;\defi\;\;  (s \domres  r) \ovl  (s \domres  q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_R}}||<math>  s \domsub  (p \bunion  q) \;\;\defi\;\;  (s \domsub  p) \bunion  (s \domsub  q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BUNION_L}}||<math>  (s \bunion  t) \domsub  r \;\;\defi\;\;  (s \domsub  r) \bunion  (t \domsub  r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_R}}||<math>  s \domsub  (p \binter  q) \;\;\defi\;\;  (s \domsub  p) \binter  (s \domsub  q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_BINTER_L}}||<math>  (s \binter  t) \domsub  r \;\;\defi\;\;  (s \domsub  r) \binter  (t \domsub  r) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_DPROD}}||<math>  A \domsub  (r \dprod  s) \;\;\defi\;\;  (A \domsub  r) \dprod  (A \domsub  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOMSUB_OVERL}}||<math>  A \domsub  (r \ovl  s) \;\;\defi\;\;  (A \domsub  r) \ovl  (A \domsub  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BUNION_R}}||<math>  r \ranres (s \bunion t) \;\;\defi\;\;  (r \ranres  s) \bunion  (r \ranres  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BUNION_L}}||<math>  (p \bunion  q) \ranres  s \;\;\defi\;\;  (p \ranres  s) \bunion  (q \ranres  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BINTER_R}}||<math>  r \ranres (s \binter t) \;\;\defi\;\;  (r \ranres  s) \binter  (r \ranres  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_BINTER_L}}||<math>  (p \binter  q) \ranres  s \;\;\defi\;\;  (p \ranres  s) \binter  (q \ranres  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_R}}||<math>  r \ranres  (s \setminus t) \;\;\defi\;\;  (r \ranres  s) \setminus (r \ranres  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANRES_SETMINUS_L}}||<math>  (p \setminus q) \ranres  s \;\;\defi\;\;  (p \ranres  s) \setminus (q \ranres  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BUNION_R}}||<math>  (r \bunion  s) \ransub  t \;\;\defi\;\;  (r \ransub  t) \bunion  (s \ransub  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BUNION_L}}||<math>  (p \bunion  q) \ransub  s \;\;\defi\;\;  (p \ransub  s) \bunion  (q \ransub  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BINTER_R}}||<math>  (r \binter  s) \ransub  t \;\;\defi\;\;  (r \ransub  t) \binter  (s \ransub  t) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RANSUB_BINTER_L}}||<math>  (p \binter  q) \ransub  s \;\;\defi\;\;  (p \ransub  s) \binter  (q \ransub  s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BUNION}}||<math>  (p \bunion  q)^{-1}  \;\;\defi\;\;  p^{-1}  \bunion  q^{-1} </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BINTER}}||<math>  (p \binter  q)^{-1}  \;\;\defi\;\;  p^{-1}  \binter  q^{-1} </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_SETMINUS}}||<math>  (r \setminus s)^{-1}  \;\;\defi\;\;  r^{-1}  \setminus s^{-1} </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_BCOMP}}||<math>  (r \bcomp  s)^{-1}  \;\;\defi\;\;  (s^{-1}  \bcomp  r^{-1} ) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_FCOMP}}||<math>  (p \fcomp q)^{-1}  \;\;\defi\;\;  (q^{-1}  \fcomp p^{-1} ) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_PPROD}}||<math>  (r \pprod  s)^{-1}  \;\;\defi\;\;  r^{-1}  \pprod  s^{-1} </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_DOMRES}}||<math>  (s \domres  r)^{-1}  \;\;\defi\;\;  r^{-1}  \ranres  s </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_DOMSUB}}||<math>  (s \domsub  r)^{-1}  \;\;\defi\;\;  r^{-1}  \ransub  s </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_RANRES}}||<math>  (r \ranres  s)^{-1}  \;\;\defi\;\;  s \domres  r^{-1} </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_CONVERSE_RANSUB}}||<math>  (r \ransub  s)^{-1}  \;\;\defi\;\;  s \domsub  r^{-1} </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOM_BUNION}}||<math>  \dom (r \bunion  s) \;\;\defi\;\;  \dom (r) \bunion  \dom (s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RAN_BUNION}}||<math>  \ran (r \bunion  s) \;\;\defi\;\;  \ran (r) \bunion  \ran (s) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_R}}||<math>  r[S \bunion  T] \;\;\defi\;\;  r[S] \bunion  r[T] </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RELIMAGE_BUNION_L}}||<math>  (p \bunion  q)[S] \;\;\defi\;\;  p[S] \bunion  q[S] </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_DOM_BUNION}}||<math>  \dom (p \bunion  q) \;\;\defi\;\;  \dom (p) \bunion  \dom (q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DISTRI_RAN_BUNION}}||<math>  \ran (p \bunion  q) \;\;\defi\;\;  \ran (p) \bunion  \ran (q) </math>||  ||  M
 +
{{RRRow}}|*||{{Rulename|DERIV_DOM_TOTALREL}}||<math>  \dom (r) \;\;\defi\;\;  E </math> || with hypothesis <math>r \in E \mathit{op} F</math>, where <math>\mathit{op}</math> is one of <math>\trel, \strel, \tfun, \tinj, \tsur, \tbij</math> ||  M
 +
{{RRRow}}| ||{{Rulename|DERIV_RAN_SURJREL}}||<math>  \ran (r) \;\;\defi\;\;  F </math> || with hypothesis <math>r \in E \mathit{op} F</math>, where <math>\mathit{op}</math> is one of <math>\srel,\strel, \psur, \tsur, \tbij</math> ||  M
 +
{{RRRow}}| ||{{Rulename|prjone-total}}||<math>  z \in \dom (\prjone) \;\;\defi\;\; \btrue </math> ||  ||  A
 +
{{RRRow}}| ||{{Rulename|prjtwo-total}}||<math>  z \in \dom (\prjtwo) \;\;\defi\;\; \btrue </math> ||  ||  A
 +
{{RRRow}}| ||{{Rulename|prjone-functional}}||<math>  \prjone \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue </math> || where \mathit{op} is one of <math> \pfun, \tfun, \trel </math> ||  A
 +
{{RRRow}}| ||{{Rulename|prjtwo-functional}}||<math>  \prjtwo \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue </math> || where \mathit{op} is one of <math> \pfun, \tfun, \trel </math> ||  A
 +
{{RRRow}}| ||{{Rulename|prj-expand}}||<math> x \;\;\defi\;\; \prjone(x) \mapsto \prjtwo(x) </math> || ||  M
  
−
'''Tutorial for the extension of the Rodin platform by plugin addition'''
+
|}
  
−
This tutorial is problem solving oriented.
 
−
In a first part, we will focus on Rodin extensions to develop a plugin for Probabilistic Termination and Qualitative Reasoning. In a second part, we will study specific problem cases and extend Rodin to solve them. More details can be found in the [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]].
 
  
−
==Outline==
 
−
* {{topic|Introduction_(How_to_extend_Rodin_Tutorial)|Introduction}}
 
  
−
''First part'' How to extend the UI?
+
[[Category:User documentation|The Proving Perspective]]
−
* {{topic|Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)|1 Creating our plug-in}}
+
[[Category:Rodin Platform|The Proving Perspective]]
−
* {{topic|Extending_the_Rodin_database_(How_to_extend_Rodin_Tutorial)|2 Contributing new elements in the Rodin database}}
+
[[Category:User manual|The Proving Perspective]]
−
* {{topic|Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)|3 Adding support for new elements in the Rodin structured editor}}
 
−
* {{topic|Extend_Rodin_EventB_Explorer(How_to_extend_Rodin_Tutorial)|4 Adding elements to the Event-B explorer}}
 
−
* {{topic|Extending_Rodin_Pretty Print Page(How_to_extend_Rodin_Tutorial)|5 Displaying added elements in the Pretty Print Page}}
 
−
* {{topic|Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)|6 Providing help}}
 
−
 
 
−
''Second part'':
 
−
* {{topic|Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|7 Extending the Static Checker}}
 
−
* {{topic|Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial)|8 Extending the Proof Obligation Generator}}
 
−
* {{topic|Adding_Reasoners(How_to_extend_Rodin_Tutorial)|9 Adding reasoners}}
 
−
 
 
−
==Projects==
 
−
The archives of the projects built in this tutorial are available here:
 
−
// '''FIXME. Add the links to the .zip files here.'''
 
−
* [http://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Tutorial/2.0/Help.zip/download<tt>Help.zip</tt>], which will be needed in section XXX.
 
−
 
 
−
{{Navigation|Next= [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]]}}
 
−
 
 
−
[[Category:Developer documentation|*Index]]
 
−
[[Category:Rodin Platform|*Index]]
 
−
[[Category:Tutorial|*Index]]
 

Revision as of 15:59, 23 November 2009

  Name Rule Side Condition A/M
*
SIMP_DOM_COMPSET
 \dom (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ x, \ldots , y\} A
*
SIMP_DOM_CONVERSE
 \dom (r^{-1} ) \;\;\defi\;\; \ran (r) A
*
SIMP_RAN_COMPSET
 \ran (\{ x \mapsto a, \ldots , y \mapsto b\} ) \;\;\defi\;\; \{ a, \ldots , b\} A
*
SIMP_RAN_CONVERSE
 \ran (r^{-1} ) \;\;\defi\;\; \dom (r) A
*
SIMP_SPECIAL_OVERL
 r \ovl \ldots \ovl \emptyset \ovl \ldots \ovl s \;\;\defi\;\; r \ovl \ldots \ovl s A
*
SIMP_MULTI_OVERL
 \begin{array}{cl} & r \ovl \ldots \ovl s \ovl \ldots \ovl s \ovl \ldots \ovl u \\ \defi & r \ovl \ldots \ovl \ldots \ovl s \ovl \ldots \ovl u \end{array} A
*
SIMP_TYPE_OVERL_CPROD
 r \ovl (\mathit{Ty} \cprod S) \;\;\defi\;\; (\mathit{Ty} \cprod S) where \mathit{Ty} is a type expression A
SIMP_SPECIAL_DOMRES_L
 \emptyset \domres r \;\;\defi\;\; \emptyset A
SIMP_SPECIAL_DOMRES_R
 S \domres \emptyset \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_DOMRES
 \mathit{Ty} \domres r \;\;\defi\;\; r where \mathit{Ty} is a type expression A
*
SIMP_MULTI_DOMRES_DOM
 \dom (r) \domres r \;\;\defi\;\; r A
*
SIMP_MULTI_DOMRES_RAN
 \ran (r) \domres r^{-1} \;\;\defi\;\; r^{-1} A
*
SIMP_DOMRES_ID
 S \domres (T \domres \id) \;\;\defi\;\; (S \binter T) \domres \id A
SIMP_SPECIAL_RANRES_R
 r \ranres \emptyset \;\;\defi\;\; \emptyset A
SIMP_SPECIAL_RANRES_L
 \emptyset \ranres S \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_RANRES
 r \ranres \mathit{Ty} \;\;\defi\;\; r where \mathit{Ty} is a type expression A
*
SIMP_MULTI_RANRES_RAN
 r \ranres \ran (r) \;\;\defi\;\; r A
*
SIMP_MULTI_RANRES_DOM
 r^{-1} \ranres \dom (r) \;\;\defi\;\; r^{-1} A
*
SIMP_RANRES_ID
 (S \domres \id) \ranres T \;\;\defi\;\; (S \binter T) \domres \id A
SIMP_SPECIAL_DOMSUB_L
 \emptyset \domsub r \;\;\defi\;\; r A
SIMP_SPECIAL_DOMSUB_R
 S \domsub \emptyset \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_DOMSUB
 \mathit{Ty} \domsub r \;\;\defi\;\; \emptyset where \mathit{Ty} is a type expression A
*
SIMP_MULTI_DOMSUB_DOM
 \dom (r) \domsub r \;\;\defi\;\; \emptyset A
*
SIMP_DOMSUB_ID
 S \domsub \id (T) \;\;\defi\;\; \id (T \setminus S) A
SIMP_SPECIAL_RANSUB_R
 r \ransub \emptyset \;\;\defi\;\; r A
SIMP_SPECIAL_RANSUB_L
 \emptyset \ransub S \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_RANSUB
 r \ransub \mathit{Ty} \;\;\defi\;\; \emptyset where \mathit{Ty} is a type expression A
*
SIMP_MULTI_RANSUB_RAN
 r \ransub \ran (r) \;\;\defi\;\; \emptyset A
*
SIMP_RANSUB_ID
 (S \domres \id) \ransub T \;\;\defi\;\; (S \setminus T) \domres \id A
SIMP_SPECIAL_FCOMP
 r \fcomp \ldots \fcomp \emptyset \fcomp \ldots \fcomp s \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_FCOMP_ID
 r \fcomp \ldots \fcomp \id \fcomp \ldots \fcomp s \;\;\defi\;\; r \fcomp \ldots \fcomp s A
*
SIMP_TYPE_FCOMP_R
 r \fcomp \mathit{Ty} \;\;\defi\;\; \dom (r) \cprod \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_TYPE_FCOMP_L
 \mathit{Ty} \fcomp r \;\;\defi\;\; \mathit{Ta} \cprod \ran (r) where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_FCOMP_ID
 r \fcomp \ldots \fcomp S \domres \id \fcomp T \domres \id \fcomp \ldots s \;\;\defi\;\; r \fcomp \ldots \fcomp (S \binter T) \domres \id \fcomp \ldots \fcomp s A
SIMP_SPECIAL_BCOMP
 r \bcomp \ldots \bcomp \emptyset \bcomp \ldots \bcomp s \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_BCOMP_ID
 r \bcomp \ldots \bcomp \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp s A
*
SIMP_TYPE_BCOMP_L
 \mathit{Ty} \bcomp r \;\;\defi\;\; \dom (r) \cprod \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_TYPE_BCOMP_R
 r \bcomp \mathit{Ty} \;\;\defi\;\; \mathit{Ta} \cprod \ran (r) where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_BCOMP_ID
 r \bcomp \ldots \bcomp S \domres \id \bcomp T \domres \id \bcomp \ldots \bcomp s \;\;\defi\;\; r \bcomp \ldots \bcomp (S \binter T) \domres \id \bcomp \ldots \bcomp s A
SIMP_SPECIAL_DPROD_R
 r \dprod \emptyset \;\;\defi\;\; \emptyset A
SIMP_SPECIAL_DPROD_L
 \emptyset \dprod r \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_DPROD
 \mathit{Ta} \dprod \mathit{Tb} \;\;\defi\;\; Tc \cprod (Td \cprod Te) where \mathit{Ta} and \mathit{Tb} are type expressions and \mathit{Ta} = \mathit{Tc} \cprod \mathit{Td} and \mathit{Tb} = \mathit{Tc} \cprod \mathit{Te} A
SIMP_SPECIAL_PPROD_R
 r \pprod \emptyset \;\;\defi\;\; \emptyset A
SIMP_SPECIAL_PPROD_L
 \emptyset \pprod r \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_PPROD
 \mathit{Ta} \pprod \mathit{Tb} \;\;\defi\;\; (Tc \cprod Te) \cprod (Td \cprod Tf) where \mathit{Ta} and \mathit{Tb} are type expressions and \mathit{Ta} = \mathit{Tc} \cprod \mathit{Td} and \mathit{Tb} = \mathit{Te} \cprod \mathit{Tf} A
*
SIMP_SPECIAL_RELIMAGE_R
 r[\emptyset ] \;\;\defi\;\; \emptyset A
SIMP_SPECIAL_RELIMAGE_L
 \emptyset [S] \;\;\defi\;\; \emptyset A
*
SIMP_TYPE_RELIMAGE
 r[Ty] \;\;\defi\;\; \ran (r) where \mathit{Ty} is a type expression A
*
SIMP_MULTI_RELIMAGE_DOM
 r[\dom (r)] \;\;\defi\;\; \ran (r) A
*
SIMP_TYPE_RELIMAGE_ID
 \id[T] \;\;\defi\;\; T A
*
SIMP_RELIMAGE_ID
 (S \domres \id)[T] \;\;\defi\;\; S \binter T A
*
SIMP_MULTI_RELIMAGE_CPROD_SING
 (\{ E\} \cprod S)[\{ E\} ] \;\;\defi\;\; S where E is a single expression A
*
SIMP_MULTI_RELIMAGE_SING_MAPSTO
 \{ E \mapsto F\} [\{ E\} ] \;\;\defi\;\; \{ F\} where E is a single expression A
*
SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB
 (r \ransub S)^{-1} [S] \;\;\defi\;\; \emptyset A
*
SIMP_MULTI_RELIMAGE_CONVERSE_RANRES
 (r \ranres S)^{-1} [S] \;\;\defi\;\; r^{-1} [S] A
*
SIMP_RELIMAGE_CONVERSE_DOMSUB
 (S \domsub r)^{-1} [T] \;\;\defi\;\; r^{-1} [T] \setminus S A
*
DERIV_RELIMAGE_RANSUB
 (r \ransub S)[T] \;\;\defi\;\; r[T] \setminus S M
*
DERIV_RELIMAGE_RANRES
 (r \ranres S)[T] \;\;\defi\;\; r[T] \binter S M
*
SIMP_MULTI_RELIMAGE_DOMSUB
 (S \domsub r)[S] \;\;\defi\;\; \emptyset A
*
DERIV_RELIMAGE_DOMSUB
 (S \domsub r)[T] \;\;\defi\;\; r[T \setminus S] M
*
DERIV_RELIMAGE_DOMRES
 (S \domres r)[T] \;\;\defi\;\; r[S \binter T] M
SIMP_SPECIAL_CONVERSE
 \emptyset ^{-1} \;\;\defi\;\; \emptyset A
*
SIMP_CONVERSE_ID
 \id^{-1} \;\;\defi\;\; \id A
*
SIMP_TYPE_CONVERSE
 \mathit{Ty}^{-1} \;\;\defi\;\; \mathit{Tb} \cprod \mathit{Ta} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_CONVERSE_SETENUM
 \{ x \mapsto a, \ldots , y \mapsto b\} ^{-1} \;\;\defi\;\; \{ a \mapsto x, \ldots , b \mapsto y\} A
*
SIMP_CONVERSE_COMPSET
 \{ x, \ldots , y \qdot P \mid x, \ldots , y\} ^{-1} \;\;\defi\;\; \{ y, \ldots , x \qdot P \mid y, \ldots , x\} A
SIMP_SPECIAL_ID
 \emptyset \domres \id \;\;\defi\;\; \emptyset A
*
SIMP_DOM_ID
 \dom (\id) \;\;\defi\;\; S where \id has type \pow(S \cprod S) A
*
SIMP_RAN_ID
 \ran (\id) \;\;\defi\;\; S where \id has type \pow(S \cprod S) A
*
SIMP_FCOMP_ID_L
 (S \domres \id) \fcomp r \;\;\defi\;\; S \domres r A
*
SIMP_FCOMP_ID_R
 r \fcomp (S \domres \id) \;\;\defi\;\; r \ranres S A
SIMP_SPECIAL_REL_R
 S \rel \emptyset \;\;\defi\;\; \{ \emptyset \} idem for operators \srel \pfun \pinj \psur A
SIMP_SPECIAL_REL_L
 \emptyset \rel S \;\;\defi\;\; \{ \emptyset \} idem for operators \trel \pfun \tfun \pinj \tinj 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 operators \tfun \tinj \tsur \tbij A
SIMP_SPECIAL_PRJ1
 \emptyset \domres \prjone \;\;\defi\;\; \emptyset A
SIMP_SPECIAL_PRJ2
 \emptyset \domres \prjtwo \;\;\defi\;\; \emptyset A
*
SIMP_FUNIMAGE_PRJ1
 \prjone (E \mapsto F) \;\;\defi\;\; E A
*
SIMP_FUNIMAGE_PRJ2
 \prjtwo (E \mapsto F) \;\;\defi\;\; F A
*
SIMP_DOM_PRJ1
 \dom (\prjone) \;\;\defi\;\; S \cprod T where \prjone has type \pow(S \cprod T \cprod S) A
*
SIMP_DOM_PRJ2
 \dom (\prjtwo) \;\;\defi\;\; S \cprod T where \prjtwo has type \pow(S \cprod T \cprod T) A
*
SIMP_RAN_PRJ1
 \ran (\prjone) \;\;\defi\;\; S where \prjone has type \pow(S \cprod T \cprod S) A
*
SIMP_RAN_PRJ2
 \ran (\prjtwo) \;\;\defi\;\; T where \prjtwo has type \pow(S \cprod T \cprod T) A
SIMP_SPECIAL_LAMBDA
 (\lambda x \qdot \bfalse \mid E) \;\;\defi\;\; \emptyset A
*
SIMP_FUNIMAGE_LAMBDA
 (\lambda x \qdot P(x) \mid E(x))(y) \;\;\defi\;\; E(y) A
*
SIMP_DOM_LAMBDA
 \dom (\lambda x \qdot P \mid E) \;\;\defi\;\; \{ x\qdot P \mid x\} A
*
SIMP_RAN_LAMBDA
 \ran (\lambda x \qdot P \mid E) \;\;\defi\;\; \{ x\qdot P \mid E\} A
*
SIMP_MULTI_FUNIMAGE_SETENUM_LL
 \{ A \mapsto E, \ldots , B \mapsto E\} (x) \;\;\defi\;\; E A
*
SIMP_MULTI_FUNIMAGE_SETENUM_LR
 \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} (x) \;\;\defi\;\; y A
*
SIMP_MULTI_FUNIMAGE_OVERL_SETENUM
 (r \ovl \ldots \ovl \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} )(x) \;\;\defi\;\; y A
*
SIMP_MULTI_FUNIMAGE_BUNION_SETENUM
 (r \bunion \ldots \bunion \{ A \mapsto E, \ldots , x \mapsto y, \ldots , B \mapsto F\} )(x) \;\;\defi\;\; y A
*
SIMP_FUNIMAGE_CPROD
 (S \cprod \{ F\} )(x) \;\;\defi\;\; F A
*
SIMP_FUNIMAGE_ID
 \id (x) \;\;\defi\;\; x A
*
SIMP_FUNIMAGE_FUNIMAGE_CONVERSE
 f(f^{-1} (E)) \;\;\defi\;\; E A
*
SIMP_FUNIMAGE_CONVERSE_FUNIMAGE
 f^{-1}(f(E)) \;\;\defi\;\; E A
*
SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM
 \{x \mapsto a, \ldots, y \mapsto b\}(\{a \mapsto x, \ldots, b \mapsto y\}(E)) \;\;\defi\;\; E A
*
DEF_BCOMP
 r \bcomp \ldots \bcomp s \;\;\defi\;\; s \fcomp \ldots \fcomp r M
*
DERIV_ID_SING
 \{ E\} \domres \id \;\;\defi\;\; \{ E \mapsto E\} where E is a single expression M
*
SIMP_SPECIAL_DOM
 \dom (\emptyset ) \;\;\defi\;\; \emptyset A
*
SIMP_SPECIAL_RAN
 \ran (\emptyset ) \;\;\defi\;\; \emptyset A
*
SIMP_CONVERSE_CONVERSE
 r^{-1-1} \;\;\defi\;\; r A
*
DERIV_RELIMAGE_FCOMP
 (p \fcomp q)[s] \;\;\defi\;\; q[p[s]] M
*
DERIV_FCOMP_DOMRES
 (s \domres p) \fcomp q \;\;\defi\;\; s \domres (p \fcomp q) M
*
DERIV_FCOMP_DOMSUB
 (s \domsub p) \fcomp q \;\;\defi\;\; s \domsub (p \fcomp q) M
*
DERIV_FCOMP_RANRES
 p \fcomp (q \ranres s) \;\;\defi\;\; (p \fcomp q) \ranres s M
*
DERIV_FCOMP_RANSUB
 p \fcomp (q \ransub s) \;\;\defi\;\; (p \fcomp q) \ransub s M
SIMP_SPECIAL_EQUAL_RELDOMRAN
 \emptyset \strel \emptyset \;\;\defi\;\; \{ \emptyset \} idem for operators \tsur \tbij A
*
SIMP_TYPE_DOM
 \dom (\mathit{Ty}) \;\;\defi\;\; \mathit{Ta} where \mathit{Ty} is a type expression equal to \mathit{Ta} \rel \mathit{Tb} A
*
SIMP_TYPE_RAN
 \ran (\mathit{Ty}) \;\;\defi\;\; \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \rel \mathit{Tb} A
*
SIMP_MULTI_DOM_CPROD
 \dom (E \cprod E) \;\;\defi\;\; E A
*
SIMP_MULTI_RAN_CPROD
 \ran (E \cprod E) \;\;\defi\;\; E A
*
DEF_IN_DOM
 E \in \dom (r) \;\;\defi\;\; \exists y \qdot E \mapsto y \in r M
*
DEF_IN_RAN
 F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r M
*
DEF_IN_CONVERSE
 E \mapsto F \in r^{-1} \;\;\defi\;\; F \mapsto E \in r M
*
DEF_IN_DOMRES
 E \mapsto F \in S \domres r \;\;\defi\;\; E \in S \land E \mapsto F \in r M
*
DEF_IN_RANRES
 E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \in T M
*
DEF_IN_DOMSUB
 E \mapsto F \in S \domsub r \;\;\defi\;\; E \notin S \land E \mapsto F \in r M
*
DEF_IN_RANSUB
 E \mapsto F \in r \ranres T \;\;\defi\;\; E \mapsto F \in r \land F \notin T M
*
DEF_IN_RELIMAGE
 F \in r[w] \;\;\defi\;\; \exists x \qdot x \in w \land x \mapsto F \in r M
*
DEF_IN_FCOMP
 E \mapsto F \in (p \fcomp q) \;\;\defi\;\; \exists x \qdot E \mapsto x \in p \land x \mapsto F \in q M
*
DEF_OVERL
 p \ovl q \;\;\defi\;\; (\dom (q) \domsub p) \bunion q M
*
DEF_IN_ID
 E \mapsto F \in \id \;\;\defi\;\; E = F M
*
DEF_IN_DPROD
 E \mapsto (F \mapsto G) \in p \dprod q \;\;\defi\;\; E \mapsto F \in p \land E \mapsto G \in q M
*
DEF_IN_PPROD
 (E \mapsto G) \mapsto (F \mapsto H) \in p \pprod q \;\;\defi\;\; E \mapsto F \in p \land G \mapsto H \in q M
*
DEF_IN_RELDOM
 r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S M
*
DEF_IN_RELRAN
 r \in S \trel T \;\;\defi\;\; r \in S \rel T \land \ran (r) = T M
*
DEF_IN_RELDOMRAN
 r \in S \strel T \;\;\defi\;\; r \in S \rel T \land \dom (r) = S \land \ran (r) = T M
*
DEF_IN_FCT
 \begin{array}{rcl} f \in S \pfun T & \defi & f \in S \rel T \\ & \land & (\forall x,y,z \qdot x \mapsto y \in f \land x \mapsto z \in f \limp y = z) \\ \end{array} M
*
DEF_IN_TFCT
 f \in S \tfun T \;\;\defi\;\; f \in S \pfun T \land \dom (f) = S M
*
DEF_IN_INJ
 f \in S \pinj T \;\;\defi\;\; f \in S \pfun T \land f^{-1} \in T \pfun S M
*
DEF_IN_TINJ
 f \in S \tinj T \;\;\defi\;\; f \in S \pinj T \land \dom (f) = S M
*
DEF_IN_SURJ
 f \in S \pfun T \;\;\defi\;\; f \in S \pfun T \land \ran (f) = T M
*
DEF_IN_TSURJ
 f \in S \tsur T \;\;\defi\;\; f \in S \psur T \land \dom (f) = S M
*
DEF_IN_BIJ
 f \in S \tbij T \;\;\defi\;\; f \in S \tinj T \land \ran (f) = T M
*
DISTRI_BCOMP_BUNION
 r \bcomp (s \bunion t) \;\;\defi\;\; (r \bcomp s) \bunion (r \bcomp s) M
*
DISTRI_FCOMP_BUNION_R
 p \fcomp (q \bunion r) \;\;\defi\;\; (p \fcomp q) \bunion (p \fcomp r) M
*
DISTRI_FCOMP_BUNION_L
 (q \bunion r) \fcomp p \;\;\defi\;\; (q \fcomp p) \bunion (r \fcomp p) M
*
DISTRI_DPROD_BUNION
 r \dprod (s \bunion t) \;\;\defi\;\; (r \dprod s) \bunion (r \dprod t) M
*
DISTRI_DPROD_BINTER
 r \dprod (s \binter t) \;\;\defi\;\; (r \dprod s) \binter (r \dprod t) M
*
DISTRI_DPROD_SETMINUS
 r \dprod (s \setminus t) \;\;\defi\;\; (r \dprod s) \setminus (r \dprod t) M
*
DISTRI_DPROD_OVERL
 r \dprod (s \ovl t) \;\;\defi\;\; (r \dprod s) \ovl (r \dprod t) M
*
DISTRI_PPROD_BUNION
 r \pprod (s \bunion t) \;\;\defi\;\; (r \pprod s) \bunion (r \pprod t) M
*
DISTRI_PPROD_BINTER
 r \pprod (s \binter t) \;\;\defi\;\; (r \pprod s) \binter (r \pprod t) M
*
DISTRI_PPROD_SETMINUS
 r \pprod (s \setminus t) \;\;\defi\;\; (r \pprod s) \setminus (r \pprod t) M
*
DISTRI_PPROD_OVERL
 r \pprod (s \ovl t) \;\;\defi\;\; (r \pprod s) \ovl (r \pprod t) M
*
DISTRI_OVERL_BUNION_L
 (p \bunion q) \ovl r \;\;\defi\;\; (p \ovl r) \bunion (q \ovl r) M
*
DISTRI_OVERL_BINTER_L
 (p \binter q) \ovl r \;\;\defi\;\; (p \ovl r) \binter (q \ovl r) M
*
DISTRI_DOMRES_BUNION_R
 s \domres (p \bunion q) \;\;\defi\;\; (s \domres p) \bunion (s \domres q) M
*
DISTRI_DOMRES_BUNION_L
 (s \bunion t) \domres r \;\;\defi\;\; (s \domres r) \bunion (t \domres r) M
*
DISTRI_DOMRES_BINTER_R
 s \domres (p \binter q) \;\;\defi\;\; (s \domres p) \binter (s \domres q) M
*
DISTRI_DOMRES_BINTER_L
 (s \binter t) \domres r \;\;\defi\;\; (s \domres r) \binter (t \domres r) M
*
DISTRI_DOMRES_SETMINUS_R
 s \domres (p \setminus q) \;\;\defi\;\; (s \domres p) \setminus (s \domres q) M
*
DISTRI_DOMRES_SETMINUS_L
 (s \setminus t) \domres r \;\;\defi\;\; (s \domres r) \setminus (t \domres r) M
*
DISTRI_DOMRES_DPROD
 s \domres (p \dprod q) \;\;\defi\;\; (s \domres p) \dprod (s \domres q) M
*
DISTRI_DOMRES_OVERL
 s \domres (r \ovl q) \;\;\defi\;\; (s \domres r) \ovl (s \domres q) M
*
DISTRI_DOMSUB_BUNION_R
 s \domsub (p \bunion q) \;\;\defi\;\; (s \domsub p) \bunion (s \domsub q) M
*
DISTRI_DOMSUB_BUNION_L
 (s \bunion t) \domsub r \;\;\defi\;\; (s \domsub r) \bunion (t \domsub r) M
*
DISTRI_DOMSUB_BINTER_R
 s \domsub (p \binter q) \;\;\defi\;\; (s \domsub p) \binter (s \domsub q) M
*
DISTRI_DOMSUB_BINTER_L
 (s \binter t) \domsub r \;\;\defi\;\; (s \domsub r) \binter (t \domsub r) M
*
DISTRI_DOMSUB_DPROD
 A \domsub (r \dprod s) \;\;\defi\;\; (A \domsub r) \dprod (A \domsub s) M
*
DISTRI_DOMSUB_OVERL
 A \domsub (r \ovl s) \;\;\defi\;\; (A \domsub r) \ovl (A \domsub s) M
*
DISTRI_RANRES_BUNION_R
 r \ranres (s \bunion t) \;\;\defi\;\; (r \ranres s) \bunion (r \ranres t) M
*
DISTRI_RANRES_BUNION_L
 (p \bunion q) \ranres s \;\;\defi\;\; (p \ranres s) \bunion (q \ranres s) M
*
DISTRI_RANRES_BINTER_R
 r \ranres (s \binter t) \;\;\defi\;\; (r \ranres s) \binter (r \ranres t) M
*
DISTRI_RANRES_BINTER_L
 (p \binter q) \ranres s \;\;\defi\;\; (p \ranres s) \binter (q \ranres s) M
*
DISTRI_RANRES_SETMINUS_R
 r \ranres (s \setminus t) \;\;\defi\;\; (r \ranres s) \setminus (r \ranres t) M
*
DISTRI_RANRES_SETMINUS_L
 (p \setminus q) \ranres s \;\;\defi\;\; (p \ranres s) \setminus (q \ranres s) M
*
DISTRI_RANSUB_BUNION_R
 (r \bunion s) \ransub t \;\;\defi\;\; (r \ransub t) \bunion (s \ransub t) M
*
DISTRI_RANSUB_BUNION_L
 (p \bunion q) \ransub s \;\;\defi\;\; (p \ransub s) \bunion (q \ransub s) M
*
DISTRI_RANSUB_BINTER_R
 (r \binter s) \ransub t \;\;\defi\;\; (r \ransub t) \binter (s \ransub t) M
*
DISTRI_RANSUB_BINTER_L
 (p \binter q) \ransub s \;\;\defi\;\; (p \ransub s) \binter (q \ransub s) M
*
DISTRI_CONVERSE_BUNION
 (p \bunion q)^{-1} \;\;\defi\;\; p^{-1} \bunion q^{-1} M
*
DISTRI_CONVERSE_BINTER
 (p \binter q)^{-1} \;\;\defi\;\; p^{-1} \binter q^{-1} M
*
DISTRI_CONVERSE_SETMINUS
 (r \setminus s)^{-1} \;\;\defi\;\; r^{-1} \setminus s^{-1} M
*
DISTRI_CONVERSE_BCOMP
 (r \bcomp s)^{-1} \;\;\defi\;\; (s^{-1} \bcomp r^{-1} ) M
*
DISTRI_CONVERSE_FCOMP
 (p \fcomp q)^{-1} \;\;\defi\;\; (q^{-1} \fcomp p^{-1} ) M
*
DISTRI_CONVERSE_PPROD
 (r \pprod s)^{-1} \;\;\defi\;\; r^{-1} \pprod s^{-1} M
*
DISTRI_CONVERSE_DOMRES
 (s \domres r)^{-1} \;\;\defi\;\; r^{-1} \ranres s M
*
DISTRI_CONVERSE_DOMSUB
 (s \domsub r)^{-1} \;\;\defi\;\; r^{-1} \ransub s M
*
DISTRI_CONVERSE_RANRES
 (r \ranres s)^{-1} \;\;\defi\;\; s \domres r^{-1} M
*
DISTRI_CONVERSE_RANSUB
 (r \ransub s)^{-1} \;\;\defi\;\; s \domsub r^{-1} M
*
DISTRI_DOM_BUNION
 \dom (r \bunion s) \;\;\defi\;\; \dom (r) \bunion \dom (s) M
*
DISTRI_RAN_BUNION
 \ran (r \bunion s) \;\;\defi\;\; \ran (r) \bunion \ran (s) M
*
DISTRI_RELIMAGE_BUNION_R
 r[S \bunion T] \;\;\defi\;\; r[S] \bunion r[T] M
*
DISTRI_RELIMAGE_BUNION_L
 (p \bunion q)[S] \;\;\defi\;\; p[S] \bunion q[S] M
*
DISTRI_DOM_BUNION
 \dom (p \bunion q) \;\;\defi\;\; \dom (p) \bunion \dom (q) M
*
DISTRI_RAN_BUNION
 \ran (p \bunion q) \;\;\defi\;\; \ran (p) \bunion \ran (q) M
*
DERIV_DOM_TOTALREL
 \dom (r) \;\;\defi\;\; E with hypothesis r \in E \mathit{op} F, where \mathit{op} is one of \trel, \strel, \tfun, \tinj, \tsur, \tbij M
DERIV_RAN_SURJREL
 \ran (r) \;\;\defi\;\; F with hypothesis r \in E \mathit{op} F, where \mathit{op} is one of \srel,\strel, \psur, \tsur, \tbij M
prjone-total
 z \in \dom (\prjone) \;\;\defi\;\; \btrue A
prjtwo-total
 z \in \dom (\prjtwo) \;\;\defi\;\; \btrue A
prjone-functional
 \prjone \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue where \mathit{op} is one of \pfun, \tfun, \trel A
prjtwo-functional
 \prjtwo \in E\ \mathit{op}\ F \;\;\defi\;\; \btrue where \mathit{op} is one of \pfun, \tfun, \trel A
prj-expand
 x \;\;\defi\;\; \prjone(x) \mapsto \prjtwo(x) M
Retrieved from ‘https://wiki.event-b.org/index.php?title=Plug-in_Tutorial&oldid=6830’