Difference between pages "Set Rewrite Rules" and "Theory Plug-in"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Josselin
(Removed SIMP_TYPE_EQUAL_EMPTY (moved to Empty Set Rewrite Rules))
 
(Add to Theory Plug-in category)
 
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
Return to [[Rodin Plug-ins]]
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]].
 
  
{{RRHeader}}
+
See also [[Theory Release History]]
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BTRUE}}||<math>  P \land  \ldots  \land  \btrue  \land  \ldots  \land  Q \;\;\defi\;\;  P \land  \ldots  \land  Q </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_AND_BFALSE}}||<math>  P \land  \ldots  \land  \bfalse  \land  \ldots  \land  Q \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_AND}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  Q \land  \ldots  \land  R \;\;\defi\;\;  P \land  \ldots  \land  Q \land  \ldots  \land  R </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_AND_NOT}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BTRUE}}||<math>  P \lor  \ldots  \lor  \btrue  \lor  \ldots  \lor  Q \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_OR_BFALSE}}||<math>  P \lor  \ldots  \lor  \bfalse  \lor  \ldots  \lor  Q \;\;\defi\;\;  P \lor  \ldots  \lor  Q </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_OR}}||<math>  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  Q \lor  \ldots  \lor  R \;\;\defi\;\;  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  R </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_OR_NOT}}||<math>  P \lor  \ldots  \lor  Q \lor  \ldots  \lor  \lnot\, Q \land  \ldots  \land  R \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_R}}||<math>  P \limp  \btrue  \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BTRUE_L}}||<math>  \btrue  \limp  P \;\;\defi\;\;  P </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BFALSE_R}}||<math>  P \limp  \bfalse  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IMP_BFALSE_L}}||<math>  \bfalse  \limp  P \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP}}||<math>  P \limp  P \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_NOT_L}}||<math>\lnot P\limp P\;\;\defi\;\; P</math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_NOT_R}}||<math>P\limp\lnot P\;\;\defi\;\;\lnot P</math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_AND}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  R \limp  Q \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_AND_NOT_R}}||<math>  P \land  \ldots  \land  Q \land  \ldots  \land  R \limp  \lnot\, Q \;\;\defi\;\;  \lnot\,(P \land  \ldots  \land  Q \land  \ldots  \land  R) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IMP_AND_NOT_L}}||<math>  P \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R \limp  Q \;\;\defi\;\;  \lnot\,(P \land  \ldots  \land  \lnot\, Q \land  \ldots  \land  R) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQV}}||<math>  P \leqv  P \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQV_NOT}}||<math>  P \leqv  \lnot\, P \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BTRUE}}||<math>  \lnot\, \btrue  \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_BFALSE}}||<math>  \lnot\, \bfalse  \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOT_NOT}}||<math>  \lnot\, \lnot\, P \;\;\defi\;\;  P </math>||  ||  AM
 
{{RRRow}}|*||{{Rulename|SIMP_NOTEQUAL}}||<math>  E \neq  F \;\;\defi\;\;  \lnot\, E = F </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOTIN}}||<math>  E \notin  F \;\;\defi\;\;  \lnot\, E \in  F </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOTSUBSET}}||<math>  E  \not\subset  F \;\;\defi\;\;  \lnot\, E  \subset  F </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOTSUBSETEQ}}||<math>  E  \not\subseteq  F \;\;\defi\;\;  \lnot\, E \subseteq  F </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOT_LE}}||<math>  \lnot\, a \leq  b \;\;\defi\;\;  a > b </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOT_GE}}||<math>  \lnot\, a \geq  b \;\;\defi\;\;  a < b </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOT_LT}}||<math>  \lnot\, a < b \;\;\defi\;\;  a \geq  b </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_NOT_GT}}||<math>  \lnot\, a > b \;\;\defi\;\;  a \leq  b </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_FALSE_R}}||<math>  \lnot\, (E = \False ) \;\;\defi\;\;  (E = \True ) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_FALSE_L}}||<math>  \lnot\, (\False  = E) \;\;\defi\;\;  (\True  = E) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_TRUE_R}}||<math>  \lnot\, (E = \True ) \;\;\defi\;\;  (E = \False ) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_NOT_EQUAL_TRUE_L}}||<math>  \lnot\, (\True  = E) \;\;\defi\;\;  (\False  = E) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FORALL_AND}}||<math>  \forall x \qdot  P \land  Q \;\;\defi\;\;  (\forall x \qdot  P) \land  (\forall x \qdot  Q) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_EXISTS_OR}}||<math>  \exists x \qdot  P \lor  Q \;\;\defi\;\;  (\exists x \qdot  P) \lor  (\exists x \qdot  Q) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_EXISTS_IMP}}||<math>\exists x\qdot P\limp Q\;\;\defi\;\;(\forall x\qdot P)\limp(\exists x\qdot Q)</math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FORALL}}||<math>  \forall \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \forall z \qdot  P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_EXISTS}}||<math>  \exists \ldots ,z,\ldots  \qdot  P(z) \;\;\defi\;\;  \exists z \qdot  P(z) </math>|| Quantified identifiers other than <math>z</math> do not occur in <math>P</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL}}||<math>  E = E \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_NOTEQUAL}}||<math>  E \neq  E \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_MAPSTO}}||<math>  E \mapsto  F = G \mapsto  H \;\;\defi\;\;  E = G \land  F = H </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_SING}}||<math>  \{ E\}  = \{ F\}  \;\;\defi\;\;  E = F </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_TRUE}}||<math>  \True  = \False  \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SUBSETEQ}}||<math>  S \subseteq  \mathit{Ty} \;\;\defi\;\;  \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_SING}}||<math>  \{ E\}  \subseteq  S \;\;\defi\;\;  E \in  S </math>|| where <math>E</math> is a single expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSETEQ}}||<math>  \emptyset  \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSETEQ}}||<math>  S \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BUNION}}||<math>  S \subseteq  A \bunion  \ldots  \bunion  S \bunion  \ldots  \bunion  B \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_BINTER}}||<math>  A \binter  \ldots  \binter  S \binter  \ldots  \binter  B \subseteq  S \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BUNION}}||<math>  A \bunion  \ldots  \bunion  B \subseteq  S \;\;\defi\;\;  A \subseteq  S \land  \ldots  \land  B \subseteq  S </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_BINTER}}||<math>  S \subseteq  A \binter  \ldots  \binter  B \;\;\defi\;\;  S \subseteq  A \land  \ldots  \land  S \subseteq  B </math>||  ||  A
 
<!--
 
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BUNION}}||<math>  A \bunion  \ldots  \bunion  B  \subset  S \;\;\defi\;\;  A  \subset  S \land  \ldots  \land  B  \subset  S </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_SUBSET_BINTER}}||<math>  S  \subset  A \binter  \ldots  \binter  B \;\;\defi\;\;  S  \subset  A \land  \ldots  \land  S  \subset  B </math>||  ||  A
 
-->
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_IN}}||<math>  E \in  \emptyset  \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_IN}}||<math>  B \in  \{ A, \ldots , B, \ldots , C\}  \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_IN_SING}}||<math>  E \in  \{ F\}  \;\;\defi\;\;  E = F </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SETENUM}}||<math>  \{ A, \ldots , B, \ldots , B, \ldots , C\}  \;\;\defi\;\;  \{ A, \ldots , B, \ldots , C\} </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_BINTER}}||<math>  S \binter  \ldots  \binter  \emptyset  \binter  \ldots  \binter  T \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BINTER}}||<math>  S \binter  \ldots  \binter  \mathit{Ty} \binter  \ldots  \binter  T \;\;\defi\;\;  S \binter  \ldots  \binter  T </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BINTER}}||<math>  S \binter  \ldots  \binter  T \binter  \ldots  \binter  T \binter  \ldots  \binter  U \;\;\defi\;\;  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL_BINTER}}||<math>  S \binter  \ldots  \binter  T \binter  \ldots  \binter  U = T \;\;\defi\;\;  T \subseteq  S \binter  \ldots  \binter  U </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_BUNION}}||<math>  S \bunion  \ldots  \bunion  \emptyset  \bunion  \ldots  \bunion  T \;\;\defi\;\;  S \bunion  \ldots  \bunion  T </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_BUNION}}||<math>  S \bunion  \ldots  \bunion  \mathit{Ty} \bunion  \ldots  \bunion  T \;\;\defi\;\;  \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_BUNION}}||<math>  S \bunion  \ldots  \bunion T \bunion  \ldots  \bunion T \bunion \ldots  \bunion  U \;\;\defi\;\;  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_EQUAL_BUNION}}||<math>  S \bunion  \ldots  \bunion  T \bunion  \ldots  \bunion  U = T \;\;\defi\;\;  S \bunion  \ldots  \bunion  U \subseteq  T </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SETMINUS}}||<math>  S \setminus S \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SETMINUS_R}}||<math>  S \setminus \emptyset  \;\;\defi\;\;  S </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SETMINUS_L}}||<math>  \emptyset  \setminus S \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS}}||<math>  S \setminus \mathit{Ty} \;\;\defi\;\;  \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SETMINUS_SETMINUS}}||<math> \mathit{Ty} \setminus (\mathit{Ty} \setminus S) \;\;\defi\;\;  S </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_KUNION_POW}}||<math>  \union (\pow (S)) \;\;\defi\;\;  S </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_KUNION_POW1}}||<math>  \union (\pown (S)) \;\;\defi\;\;  S </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KUNION}}||<math>  \union (\{ \emptyset \} ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_QUNION}}||<math>  \Union  x\qdot  \bfalse  \mid  E \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KINTER}}||<math>  \inter (\{ \emptyset \} ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_KINTER_POW}}||<math>  \inter (\pow (S)) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_POW}}||<math>  \pow (\emptyset ) \;\;\defi\;\;  \{ \emptyset \} </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_POW1}}||<math>  \pown (\emptyset ) \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CPROD_R}}||<math>  S \cprod  \emptyset  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_CPROD_L}}||<math>  \emptyset  \cprod  S \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|||{{Rulename|SIMP_COMPSET_EQUAL}}||<math>  \{ x, y \qdot x = E(y) \land P(y) \mid F(x, y) \}  \;\;\defi\;\;  \{ y \qdot P(y) \mid F(E(y), y) \} </math>|| where <math>x</math> non free in <math>E</math> and non free in <math>P</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_COMPSET_IN}}||<math>  \{  x \qdot  x \in  S \mid  x \}  \;\;\defi\;\;  S </math>|| where <math>x</math> non free in <math>S</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_COMPSET_SUBSETEQ}}||<math>  \{  x \qdot  x \subseteq  S \mid  x \}  \;\;\defi\;\;  \pow (S)  </math>|| where <math>x</math> non free in <math>S</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BFALSE}}||<math>  \{  x \qdot  \bfalse  \mid  x \}  \;\;\defi\;\;  \emptyset </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COMPSET_BTRUE}}||<math>  \{  x \qdot  \btrue  \mid  E \}  \;\;\defi\;\;  \mathit{Ty} </math>|| where the type of <math>E</math> is <math>\mathit{Ty}</math> and <math>E</math> is a maplet combination of locally-bound, pairwise-distinct bound identifiers ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SUBSETEQ_COMPSET_L}}||<math>  \{  x \qdot  P(x) \mid  E(x) \}  \subseteq  S \;\;\defi\;\;  \forall y\qdot  P(y) \limp  E(y) \in  S </math>|| where <math>y</math> is fresh ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET}}||<math>  F \in  \{  x,y,\ldots \qdot  P(x,y,\ldots) \mid  E(x,y,\ldots) \}  \;\;\defi\;\;  \exists x,y,\ldots \qdot P(x,y,\ldots) \land E(x,y,\ldots) = F </math>|| where <math>x</math>, <math>y</math>, <math>\ldots</math> are not free in <math>F</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_IN_COMPSET_ONEPOINT}}||<math>  E \in  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  P(E) </math>|| Equivalent to general simplification followed by One Point Rule application with the last conjunct predicate ||  A
 
{{RRRow}}|||{{Rulename|SIMP_SUBSETEQ_COMPSET_R}}||<math>  S \subseteq  \{  x \qdot  P(x) \mid  x \}  \;\;\defi\;\;  \forall y\qdot  y \in  S \limp  P(y) </math>|| where <math>y</math> non free in <math>S, \{  x \qdot  P(x) \mid  x \}</math> ||  M
 
{{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_SPECIAL_KBOOL_BTRUE}}||<math>  \bool (\btrue ) \;\;\defi\;\;  \True </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_KBOOL_BFALSE}}||<math>  \bool (\bfalse ) \;\;\defi\;\;  \False </math>||  ||  A
 
{{RRRow}}|||{{Rulename|DISTRI_SUBSETEQ_BUNION_SING}}||<math>  S \bunion  \{ F\}  \subseteq  T \;\;\defi\;\;  S \subseteq  T \land  F \in  T </math>|| where <math>F</math> is a single expression ||  M
 
{{RRRow}}|*||{{Rulename|DEF_FINITE}}||<math>  \finite(S) \;\;\defi\;\;  \exists n,f\qdot f\in 1\upto n \tbij S </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_FINITE}}||<math>  \finite (\emptyset ) \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_SETENUM}}||<math>  \finite (\{ a, \ldots , b\} ) \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_BUNION}}||<math>  \finite (S \bunion  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) </math>||  ||  A
 
{{RRRow}}| ||{{Rulename|SIMP_FINITE_UNION}}||<math>\finite(\union(S)) \;\;\defi\;\; \finite(S)\;\land\;(\forall x\qdot x\in S\limp finite(x))</math>||  ||  M
 
{{RRRow}}| ||{{Rulename|SIMP_FINITE_QUNION}}||<math>\finite(\Union x\qdot P\mid E) \;\;\defi\;\; \finite(\{x\qdot P\mid E\})\;\land\;(\forall x\qdot P\limp finite(E))</math>||  ||  M
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_POW}}||<math>  \finite (\pow (S)) \;\;\defi\;\;  \finite (S) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|DERIV_FINITE_CPROD}}||<math>  \finite (S \cprod  T) \;\;\defi\;\;  S = \emptyset  \lor  T = \emptyset  \lor  (\finite (S) \land  \finite (T)) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_CONVERSE}}||<math>  \finite (r^{-1} ) \;\;\defi\;\;  \finite (r) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_UPTO}}||<math>  \finite (a \upto  b) \;\;\defi\;\;  \btrue </math>||  ||  A
 
<!-- Disabled rules (some are false, need more thinking to check which)
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_L}}||<math>  \finite (S \binter  T) \;\;\defi\;\;  \finite (S) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_BINTER_R}}||<math>  \finite (S \binter  T) \;\;\defi\;\;  \finite (T) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_SETMINUS}}||<math>  \finite (S \setminus T) \;\;\defi\;\;  \finite (S) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOMRES}}||<math>  \finite (S \domres  r)  \;\;\defi\;\;  \finite (r) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_RANRES}}||<math>  \finite (r \ranres  S)  \;\;\defi\;\;  \finite (r) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOMSUB}}||<math>  \finite (S \domsub  r) \;\;\defi\;\;  \finite (r) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_RANSUB}}||<math>  \finite (r \ransub  S) \;\;\defi\;\;  \finite (r) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_RELIMAGE}}||<math>  \finite (r[S]) \;\;\defi\;\;  \finite (r) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_CPROD}}||<math>  \finite (S \cprod  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_OVERL}}||<math>  \finite (r \ovl  s)  \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_REL}}||<math>  \finite (S \rel  T) \;\;\defi\;\;  \finite (S) \land  \finite (T) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_FCOMP}}||<math>  \finite (r \fcomp s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_BCOMP}}||<math>  \finite (r \bcomp  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_DPROD}}||<math>  \finite (r \dprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_PPROD}}||<math>  \finite (r \pprod  s) \;\;\defi\;\;  \finite (r) \land  \finite (s) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_COMPSET}}||<math>  \finite (\{ x \qdot  x \in  S \land  \ldots  \land  P \mid  x\} ) \;\;\defi\;\;  \finite (S) </math>|| where <math>x</math> non free in <math>S</math> ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_RAN}}||<math>  \finite (\ran (r)) \;\;\defi\;\;  \finite (r) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_DOM}}||<math>  \finite (\dom (r)) \;\;\defi\;\;  \finite (r) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|SIMP_FINITE_QINTER}}||<math>  \finite (\Inter  x \qdot  P \mid  E) \;\;\defi\;\;  \exists x \qdot  P \land  \finite (E) </math>||  ||  M
 
-->
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_ID}}||<math>  \finite (\id) \;\;\defi\;\;  \finite (S) </math>|| where <math>\id</math> has type <math>\pow(S \cprod S)</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_ID_DOMRES}}||<math>  \finite (E \domres \id) \;\;\defi\;\;  \finite (E) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ1}}||<math>  \finite (\prjone) \;\;\defi\;\;  \finite (S \cprod T) </math>|| where <math>\prjone</math> has type <math>\pow(S \cprod T \cprod S)</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ2}}||<math>  \finite (\prjtwo) \;\;\defi\;\;  \finite (S \cprod T) </math>|| where <math>\prjtwo</math> has type <math>\pow(S \cprod T \cprod T)</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ1_DOMRES}}||<math>  \finite (E \domres \prjone) \;\;\defi\;\;  \finite (E) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_PRJ2_DOMRES}}||<math>  \finite (E \domres \prjtwo) \;\;\defi\;\;  \finite (E) </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_NATURAL}}||<math>  \finite (\nat ) \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_NATURAL1}}||<math>  \finite (\natn ) \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_INTEGER}}||<math>  \finite (\intg ) \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_BOOL}}||<math>  \finite (\Bool ) \;\;\defi\;\;  \btrue </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_FINITE_LAMBDA}}||<math>  \finite(\{x\qdot P\mid E\mapsto F\}) \;\;\defi\;\;  \finite(\{x\qdot P\mid E\} ) </math>|| where <math>E</math> is a maplet combination of bound identifiers and expressions that are not bound by the comprehension set (i.e., <math>E</math> is syntactically injective) and all identifiers bound by the comprehension set that occur in <math>F</math> also occur in <math>E</math> ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_IN}}||<math>  t \in  \mathit{Ty} \;\;\defi\;\;  \btrue </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BTRUE}}||<math>  P \leqv  \btrue  \;\;\defi\;\;  P </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQV_BFALSE}}||<math>  P \leqv  \bfalse  \;\;\defi\;\;  \lnot\, P </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|DEF_SUBSET}}||<math>  A  \subset  B  \;\;\defi\;\;  A \subseteq B \land \lnot A = B </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSET_R}}||<math>  S  \subset  \emptyset  \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_SUBSET_L}}||<math>\emptyset\subset S \;\;\defi\;\;  \lnot\; S = \emptyset</math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_TYPE_SUBSET_L}}||<math>  S  \subset  \mathit{Ty} \;\;\defi\;\;  S \neq  \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_MULTI_SUBSET}}||<math>  S  \subset  S \;\;\defi\;\;  \bfalse </math>||  ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CONSTR}}||<math>  \operatorname{constr} (a_1, \ldots, a_n) = \operatorname{constr} (b_1, \ldots, b_n)  \;\;\defi\;\;  a_1 = b_1 \land \ldots \land  a_n = b_n  </math>|| where <math>\operatorname{constr}</math> is a datatype constructor ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_EQUAL_CONSTR_DIFF}}||<math>  \operatorname{constr_1} (\ldots) = \operatorname{constr_2} (\ldots)  \;\;\defi\;\;  \bfalse </math>|| where <math>\operatorname{constr_1}</math> and <math>\operatorname{constr_2}</math> are different datatype constructors ||  A
 
{{RRRow}}|*||{{Rulename|SIMP_DESTR_CONSTR}}||<math>  \operatorname{destr} (\operatorname{constr} (a_1, \ldots, a_n))  \;\;\defi\;\;  a_i  </math>|| where <math>\operatorname{destr}</math> is the datatype destructor for the i-th argument of datatype constructor <math>\operatorname{constr}</math> ||  A
 
{{RRRow}}|*||{{Rulename|DISTRI_AND_OR}}||<math>  P \land  (Q \lor  R) \;\;\defi\;\;  (P \land  Q) \lor  (P \land  R) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DISTRI_OR_AND}}||<math>  P \lor  (Q \land  R) \;\;\defi\;\;  (P \lor  Q) \land  (P \lor  R) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_OR}}||<math>  P \lor  Q \lor  \ldots  \lor  R \;\;\defi\;\;  \lnot\, P \limp  (Q \lor  \ldots  \lor  R) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_IMP}}||<math>  P \limp  Q \;\;\defi\;\;  \lnot\, Q \limp  \lnot\, P </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_IMP_IMP}}||<math>  P \limp  (Q \limp  R) \;\;\defi\;\;  P \land  Q \limp  R </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DISTRI_IMP_AND}}||<math>  P \limp  (Q \land  R) \;\;\defi\;\;  (P \limp  Q) \land  (P \limp  R) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DISTRI_IMP_OR}}||<math>  (P \lor  Q) \limp  R \;\;\defi\;\;  (P \limp  R) \land  (Q \limp  R) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_EQV}}||<math>  P \leqv  Q \;\;\defi\;\;  (P \limp  Q) \land  (Q \limp  P) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DISTRI_NOT_AND}}||<math>  \lnot\,(P \land  Q) \;\;\defi\;\;  \lnot\, P \lor  \lnot\, Q </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DISTRI_NOT_OR}}||<math>  \lnot\,(P \lor  Q) \;\;\defi\;\;  \lnot\, P \land  \lnot\, Q </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_NOT_IMP}}||<math>  \lnot\,(P \limp  Q) \;\;\defi\;\;  P \land  \lnot\, Q </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_NOT_FORALL}}||<math>  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_NOT_EXISTS}}||<math>  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_MAPSTO}}||<math>  E \mapsto  F \in  S \cprod  T \;\;\defi\;\;  E \in  S \land  F \in  T </math>||  ||  AM
 
{{RRRow}}|*||{{Rulename|DEF_IN_POW}}||<math>  E \in  \pow (S) \;\;\defi\;\;  E \subseteq  S </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_POW1}}||<math>  E \in  \pown (S) \;\;\defi\;\; E \in  \pow (S) \land S \neq \emptyset </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_SUBSETEQ}}||<math> S \subseteq T  \;\;\defi\;\;  \forall x \qdot  x \in  S \limp  x \in  T </math>|| where <math>x</math> is not free in <math>S</math> or <math>T</math> ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_BUNION}}||<math>  E \in  S \bunion  T \;\;\defi\;\;  E \in  S \lor  E \in  T </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_BINTER}}||<math>  E \in  S \binter  T \;\;\defi\;\;  E \in  S \land  E \in  T </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_SETMINUS}}||<math>  E \in  S \setminus T \;\;\defi\;\;  E \in  S \land  \lnot\,(E \in  T) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_SETENUM}}||<math>  E \in  \{ A, \ldots , B\}  \;\;\defi\;\;  E = A \lor  \ldots  \lor  E = B </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_KUNION}}||<math>  E \in  \union (S) \;\;\defi\;\;  \exists s \qdot  s \in  S \land  E \in  s </math>|| where <math>s</math> is fresh ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_QUNION}}||<math>  E \in  (\Union x \qdot P(x) \mid T(x)) \;\;\defi\;\;  \exists s \qdot P(s) \land E \in T(s) </math>|| where <math>s</math> is fresh ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_KINTER}}||<math>  E \in  \inter (S) \;\;\defi\;\;  \forall s \qdot  s \in  S \limp  E \in  s </math>|| where <math>s</math> is fresh ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_QINTER}}||<math>  E \in  (\Inter x \qdot P(x) \mid T(x)) \;\;\defi\;\;  \forall s \qdot P(s) \limp E \in T(s) </math>|| where <math>s</math> is fresh ||  M
 
{{RRRow}}|*||{{Rulename|DEF_IN_UPTO}}||<math>  E \in  a \upto b \;\;\defi\;\; a \leq E \land E \leq b  </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DISTRI_BUNION_BINTER}}||<math>  S \bunion  (T \binter  U) \;\;\defi\;\;  (S \bunion  T) \binter  (S \bunion  U) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DISTRI_BINTER_BUNION}}||<math>  S \binter  (T \bunion  U) \;\;\defi\;\;  (S \binter  T) \bunion  (S \binter  U) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|DISTRI_BINTER_SETMINUS}}||<math>  S \binter  (T \setminus U) \;\;\defi\;\;  (S \binter  T) \setminus (S \binter  U) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|DISTRI_SETMINUS_BUNION}}||<math>  S \setminus (T \bunion  U) \;\;\defi\;\;  S \setminus T \setminus U </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_BINTER}}||<math>  \mathit{Ty} \setminus (S \binter  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  (\mathit{Ty} \setminus T) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_BUNION}}||<math>  \mathit{Ty} \setminus (S \bunion  T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \binter  (\mathit{Ty} \setminus T) </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_TYPE_SETMINUS_SETMINUS}}||<math>  \mathit{Ty} \setminus (S \setminus T) \;\;\defi\;\;  (\mathit{Ty} \setminus S) \bunion  T </math>|| where <math>\mathit{Ty}</math> is a type expression ||  M
 
{{RRRow}}|||{{Rulename|DISTRI_CPROD_BINTER}}||<math>  S \cprod  (T \binter  U) \;\;\defi\;\;  (S \cprod  T) \binter  (S \cprod  U) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|DISTRI_CPROD_BUNION}}||<math>  S \cprod  (T \bunion  U) \;\;\defi\;\;  (S \cprod  T) \bunion  (S \cprod  U) </math>||  ||  M
 
{{RRRow}}|||{{Rulename|DISTRI_CPROD_SETMINUS}}||<math>  S \cprod  (T \setminus U) \;\;\defi\;\;  (S \cprod  T) \setminus (S \cprod  U) </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ}}||<math>  S \subseteq  T \;\;\defi\;\;  (\mathit{Ty} \setminus T) \subseteq  (\mathit{Ty} \setminus S) </math>|| where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_EQUAL}}||<math>  S = T \;\;\defi\;\;  S \subseteq  T \land  T \subseteq  S </math>|| where <math>\pow (\mathit{Ty})</math> is the type of <math>S</math> and <math>T</math> ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_SETMINUS_L}}||<math>  A \setminus B \subseteq  S \;\;\defi\;\;  A \subseteq  B \bunion  S </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DERIV_SUBSETEQ_SETMINUS_R}}||<math>  S \subseteq  A \setminus B \;\;\defi\;\;  S \subseteq  A \land  S \binter  B = \emptyset </math>||  ||  M
 
{{RRRow}}|*||{{Rulename|DEF_PARTITION}}||<math>  \operatorname{partition} (s, s_1, s_2, \ldots, s_n) \;\;\defi\;\;
 
  \begin{array}{ll}
 
  & s = s_1\bunion s_2\bunion\cdots\bunion s_n\\
 
\land& s_1\binter s_2 = \emptyset\\
 
\vdots\\
 
\land& s_1\binter s_n = \emptyset\\
 
\vdots\\
 
\land& s_{n-1}\binter s_n = \emptyset
 
\end{array}</math>||  ||  AM
 
|}
 
  
 +
The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities.
  
[[Category:User documentation|The Proving Perspective]]
+
===Motivation===
[[Category:Rodin Platform|The Proving Perspective]]
+
Up to Rodin v2.0, the mathematical language used in Event-B has been fixed. As such, it was not possible to define reusable polymorphic operators. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the Event-B language lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator (which was present in classical B mathematical language) and the bag operator.
[[Category:User manual|The Proving Perspective]]
+
 
 +
In Rodin v2.0, support for customised syntactic symbols was introduced. The Theory plug-in, as a result, evolved from being just a component to define rewrite rules to a versatile platform to define and validate proof and language extensions.
 +
 
 +
The latest Theory plug-in is released for Rodin v2.8.
 +
 
 +
===Overview===
 +
The Theory plug-in is a Rodin extension that provides the facility to define '''''mathematical extensions''''' as well as '''''prover extensions'''''.
 +
Mathematical extensions are new operator definitions and new datatype definitions and axiomatic definitions. Operator definitions can be expression operators (e.g., ''card'') and predicate operators (e.g., ''finite''). Datatypes extensions can be used to define enumerated datatypes (e.g., ''DIRECTION'') as well as inductive datatypes (e.g., ''Tree''). Axiomatic definitions can be used to define new data types like "REAL".
 +
 
 +
The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, axiomatic definitions, inference and rewrite rules as well as polymorphic theorems. The [http://wiki.event-b.org/images/Theory_Plugin.pdf user manual] provides a guide to developing and using theories.
 +
 
 +
=== Installation & Update ===
 +
 
 +
The installation or update for the Theory plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates) under the category "Modelling Extensions". Like always, after the installation, restarting Rodin is recommended.
 +
 
 +
===User Manual===
 +
The user manual is available here: [http://wiki.event-b.org/images/Theory_Plugin.pdf Theory User Manual]. Below is the presentation of the sequence theory which its description can be found in the user manual:
 +
 
 +
[[image:SeqTheory.png|center|thumb|1500px|'''Theory of Sequence''']]
 +
 
 +
===Standard Library===
 +
In this section, you find a set of standard theories and some models using some of these theories.
 +
 
 +
The standard library of the theories is available to download:
 +
[https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.1.zip/download here] for Rodin2.8 and
 +
[https://sourceforge.net/projects/rodin-b-sharp/files/Theory_StdLib/StandardTheory0.2.zip/download here] for Rodin3.1.
 +
This library includes:
 +
* BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.
 +
* RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.
 +
* RealTheory project: including theory of Real.
 +
 
 +
Also it includes three simple Event-B models that use some of the theories:
 +
* Data project: using SUMandPRODUCT theory
 +
* Queue project: using Seq theory
 +
* SimpleNetwork project: using closure theory
 +
 
 +
In order to keep the POs discharged, you need to install "Atelier B provers" as well.
 +
 
 +
===Capabilities===
 +
The Theory plug-in has the following capabilities:
 +
 
 +
* Theory Definition:
 +
** Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
 +
** Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is ''card''. A predicate operator is one that "returns" a predicate, an example existing predicate operator is ''finite''.
 +
** Definition of axiomatic definitions: axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms.
 +
** Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
 +
** Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
 +
** Definition of polymorphic theorems: theorems can be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
 +
** Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
 +
*Theory Deployment: this step signifies that a theory is ready for use. Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.
 +
Once a theory has been deployed to its designated project, all its extensions (mathematical and prover extensions) can be used in models.
 +
 
 +
===Insider Look===
 +
The Theory plug-in partially satisfies the requirements outlined in the following document:
 +
* [http://deploy-eprints.ecs.soton.ac.uk/80/ Abrial, Jean-Raymond and Butler, Michael and Schmalz, Matthias and Hallerstede, Stefan and Voisin, Laurent. Mathematical Extensions Proposal]
 +
 
 +
A more accurate description of the implemented functionalities of the plug-in can be found in the following document:
 +
* [http://deploy-eprints.ecs.soton.ac.uk/251/ Michael Butler, Issam Maamria. Mathematical Extensions Summary]
 +
 
 +
The following two papers describe rewriting and well-definedness issues that has to be accounted for:
 +
 
 +
* [http://eprints.ecs.soton.ac.uk/18269/ Issam Maamria, Michael Butler, Andrew Edmunds, and Abdolbaghi Rezazadeh. On an Extensible Rule-based Prover for Event-B, ABZ'2010.]
 +
* [http://eprints.ecs.soton.ac.uk/21221/ Issam Maamria, Michael Butler. Rewriting and Well-Definedness within a Proof System.]
 +
 
 +
 
 +
[[Category:Plugin]]
 +
[[Category:User documentation]]
 +
[[Category:Proof]]
 +
[[Category:Theory Plug-in]]

Latest revision as of 14:53, 14 June 2021

Return to Rodin Plug-ins

See also Theory Release History

The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This page provides useful information about the plug-in and its capabilities.

Motivation

Up to Rodin v2.0, the mathematical language used in Event-B has been fixed. As such, it was not possible to define reusable polymorphic operators. A workaround was to define any required operators as set constructs in contexts. Originally, contexts were supposed to provide a parametrization of machines. The aforementioned limitations of the Event-B language lead to users to use contexts for purposes for which they were not intentionally devised. Examples of operators that can be useful to users include the sequence operator (which was present in classical B mathematical language) and the bag operator.

In Rodin v2.0, support for customised syntactic symbols was introduced. The Theory plug-in, as a result, evolved from being just a component to define rewrite rules to a versatile platform to define and validate proof and language extensions.

The latest Theory plug-in is released for Rodin v2.8.

Overview

The Theory plug-in is a Rodin extension that provides the facility to define mathematical extensions as well as prover extensions. Mathematical extensions are new operator definitions and new datatype definitions and axiomatic definitions. Operator definitions can be expression operators (e.g., card) and predicate operators (e.g., finite). Datatypes extensions can be used to define enumerated datatypes (e.g., DIRECTION) as well as inductive datatypes (e.g., Tree). Axiomatic definitions can be used to define new data types like "REAL".

The placeholder for mathematical and prover extensions is a Theory construct which looks similar to contexts and machines. A theory can include datatypes definitions, operator definitions, axiomatic definitions, inference and rewrite rules as well as polymorphic theorems. The user manual provides a guide to developing and using theories.

Installation & Update

The installation or update for the Theory plug-in is available under the main Rodin Update site (http://rodin-b-sharp.sourceforge.net/updates) under the category "Modelling Extensions". Like always, after the installation, restarting Rodin is recommended.

User Manual

The user manual is available here: Theory User Manual. Below is the presentation of the sequence theory which its description can be found in the user manual:

Theory of Sequence

Standard Library

In this section, you find a set of standard theories and some models using some of these theories.

The standard library of the theories is available to download:

here for Rodin2.8 and
here for Rodin3.1. 

This library includes:

  • BasicTheory project: including theories of BinaryTree, BoolOps, List, PEANO, SUMandPRODUCT and Seq.
  • RelationOrderTheory project: including theories of Connectivity, FixPoint, Relation, Well_Fondation, closure, complement and galois.
  • RealTheory project: including theory of Real.

Also it includes three simple Event-B models that use some of the theories:

  • Data project: using SUMandPRODUCT theory
  • Queue project: using Seq theory
  • SimpleNetwork project: using closure theory

In order to keep the POs discharged, you need to install "Atelier B provers" as well.

Capabilities

The Theory plug-in has the following capabilities:

  • Theory Definition:
    • Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
    • Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is card. A predicate operator is one that "returns" a predicate, an example existing predicate operator is finite.
    • Definition of axiomatic definitions: axiomatic definitions are defined by supplying the types, a set of operators, and a set of axioms.
    • Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
    • Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
    • Definition of polymorphic theorems: theorems can be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
    • Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
  • Theory Deployment: this step signifies that a theory is ready for use. Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.

Once a theory has been deployed to its designated project, all its extensions (mathematical and prover extensions) can be used in models.

Insider Look

The Theory plug-in partially satisfies the requirements outlined in the following document:

A more accurate description of the implemented functionalities of the plug-in can be found in the following document:

The following two papers describe rewriting and well-definedness issues that has to be accounted for: