Difference between pages "Element Hierarchy Extension Point & Library" and "Empty Set Rewrite Rules"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Laurent
m (Change \ldots to \cdots for tall operators)
 
Line 1: Line 1:
−
The UI in Rodin 2.x contains an extension point <tt>org.eventb.ui.editorItems</tt> that groups the both following information:
+
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
−
*the definition of elements and attributes and their hierarchy, and the way they are created
+
Rules without a <tt>*</tt> are planned to be implemented in future versions.
−
*the information needed to correctly display and edit these elements in the various editors and UI components
+
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
  
−
It appears obvious that the first information should be defined from an extension that belongs to the Database.
+
All rewrite rules that match the pattern <math>\textbf{P}=\emptyset</math> are also applicable to predicates of the form <math>\textbf{P}\subseteq\emptyset</math>  and  <math>\emptyset=\textbf{P}</math>, as these predicates are equivalent. All rewrite rules that match the pattern <math>\textbf{P}=\mathit{Ty}</math> are also applicable to predicates of the form <math>\mathit{Ty}\subseteq\textbf{P}</math>  and <math>\mathit{Ty}=\textbf{P}</math>, as these predicates are equivalent.
−
To fullfil the above statement, the current extension point <tt>org.eventb.ui.editorItems</tt> should be split in two.
 
−
The existing extension point was also heterogenous. Indeed, whereas the element relationships were concerning element types, the attribute relationship were concerning element types and references to UI defined attributes (referring to core attributes).<br>
 
−
There is no need for such an indirection.
 
  
−
----
+
{{RRHeader}}
−
The proposal should concern :
+
{{RRRow}}|*||{{Rulename|DEF_SPECIAL_NOT_EQUAL}}||<math>  \lnot\, S = \emptyset  \;\;\defi\;\;  \exists x \qdot  x \in  S </math>|| where <math>x</math> is not free in <math>S</math> ||  M
−
  A - Relationship declaration (new extension point)
+
{{RRRow}}|||{{Rulename|SIMP_SETENUM_EQUAL_EMPTY}}||<math>  \{ A, \ldots , B\}  = \emptyset \;\;\defi\;\;  \bfalse </math>||  ||  A
−
  B - API to test these relations and traverse them
+
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_COMPSET}}||<math>  \{  x \qdot  P(x) \mid  E \}  = \emptyset  \;\;\defi\;\;  \forall x\qdot  \lnot\, P(x) </math>||  ||  A
−
  C - Enforcement of the authorized relations when modifying the DB
+
{{RRRow}}|||{{Rulename|SIMP_BINTER_EQUAL_TYPE}}||<math>  A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\;  A = \mathit{Ty} \land \cdots \land B  = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
−
  D- What about the compatibilty with the file upgrade mechanism?
+
{{RRRow}}|||{{Rulename|SIMP_BINTER_SING_EQUAL_EMPTY}}||<math> A \binter \{ a \}  = \emptyset  \;\;\defi\;\;  \lnot\, a \in A </math>||  ||  A
−
----
+
{{RRRow}}|||{{Rulename|SIMP_BINTER_SETMINUS_EQUAL_EMPTY}}||<math>  (A \setminus B) \binter C  = \emptyset  \;\;\defi\;\;  (A \binter C) \setminus B = \emptyset</math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_BUNION_EQUAL_EMPTY}}||<math>  A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\;  A = \emptyset \land \cdots \land B  = \emptyset </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_EMPTY}}||<math>  A \setminus  B = \emptyset \;\;\defi\;\;  A \subseteq  B  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_SETMINUS_EQUAL_TYPE}}||<math>  A \setminus B = \mathit{Ty} \;\;\defi\;\;  A = \mathit{Ty} \land B = \emptyset </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_POW_EQUAL_EMPTY}}||<math>  \pow (S) = \emptyset \;\;\defi\;\;  \bfalse  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_POW1_EQUAL_EMPTY}}||<math>  \pown (S) = \emptyset \;\;\defi\;\;  S = \emptyset  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_KINTER_EQUAL_TYPE}}||<math>  \inter (S) = \mathit{Ty} \;\;\defi\;\;  S = \{ \mathit{Ty} \}  </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_KUNION_EQUAL_EMPTY}}||<math>  \union (S) = \emptyset \;\;\defi\;\;  S \subseteq \{ \emptyset \}  </math>|| ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_QINTER_EQUAL_TYPE}}||<math>  (\Inter  x\qdot P(x)  \mid  E(x)) = \mathit{Ty} \;\;\defi\;\;  \forall x\qdot  P(x) \limp E(x) = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_QUNION_EQUAL_EMPTY}}||<math>  (\Union  x\qdot P(x)  \mid  E(x)) = \emptyset \;\;\defi\;\;  \forall x\qdot  P(x) \limp E(x) = \emptyset</math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_NATURAL_EQUAL_EMPTY}}||<math>  \nat = \emptyset \;\;\defi\;\;  \bfalse</math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_NATURAL1_EQUAL_EMPTY}}||<math>  \natn = \emptyset \;\;\defi\;\;  \bfalse</math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_TYPE_EQUAL_EMPTY}}||<math> \mathit{Ty} = \emptyset  \;\;\defi\;\;  \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_CPROD_EQUAL_EMPTY}}||<math>  S \cprod T = \emptyset \;\;\defi\;\; S = \emptyset \lor T = \emptyset </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_CPROD_EQUAL_TYPE}}||<math>  S \cprod T = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land T = \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_EMPTY}}||<math>  i \upto j = \emptyset \;\;\defi\;\; i > j </math>|| ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_INTEGER}}||<math>  i \upto j = \intg \;\;\defi\;\; \bfalse </math>|| ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_NATURAL}}||<math>  i \upto j = \nat \;\;\defi\;\; \bfalse </math>|| ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_UPTO_EQUAL_NATURAL1}}||<math>  i \upto j = \natn \;\;\defi\;\; \bfalse </math>|| ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_REL}}||<math>  A \rel  B = \emptyset  \;\;\defi\;\;  \bfalse </math>|| idem for operators <math>\pfun  \pinj</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_TYPE_EQUAL_REL}}||<math>  A \rel  B = \mathit{Ty}  \;\;\defi\;\;  A = \mathit{Ta} \land B = \mathit{Tb} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_EQUAL_RELDOM}}||<math>  A \trel  B = \emptyset  \;\;\defi\;\;  \lnot\, A = \emptyset  \land  B = \emptyset </math>|| idem for operator <math>\tfun</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_TYPE_EQUAL_RELDOMRAN}}||<math>  A \trel  B = \mathit{Ty}  \;\;\defi\;\;  \bfalse </math>|| where <math>\mathit{Ty}</math> is a type expression, idem for operator <math>\srel, \strel, \tfun, \tinj, \psur, \tsur, \tbij</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_SREL_EQUAL_EMPTY}}||<math>  A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land  \lnot\,B = \emptyset </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_STREL_EQUAL_EMPTY}}||<math>  A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv  \lnot\,B = \emptyset) </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_DOM_EQUAL_EMPTY}}||<math>  \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_RAN_EQUAL_EMPTY}}||<math>  \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_FCOMP_EQUAL_EMPTY}}||<math> p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_BCOMP_EQUAL_EMPTY}}||<math> p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_DOMRES_EQUAL_EMPTY}}||<math> S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset  </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_DOMRES_EQUAL_TYPE}}||<math> S \domres r = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land r = \mathit{Ty}  </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_DOMSUB_EQUAL_EMPTY}}||<math> S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_DOMSUB_EQUAL_TYPE}}||<math> S \domsub r = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} </math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_RANRES_EQUAL_EMPTY}}||<math> r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset</math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_RANRES_EQUAL_TYPE}}||<math> r \ranres S = \mathit{Ty} \;\;\defi\;\; S = \mathit{Tb} \land r = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod \mathit{Tb}</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_RANSUB_EQUAL_EMPTY}}||<math> r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S </math>|| ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_RANSUB_EQUAL_TYPE}}||<math> r \ransub S = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty}</math>|| where <math>\mathit{Ty}</math> is a type expression || A
 +
{{RRRow}}|||{{Rulename|SIMP_CONVERSE_EQUAL_EMPTY}}||<math> r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset</math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_CONVERSE_EQUAL_TYPE}}||<math> r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1}</math>|| where <math>\mathit{Ty}</math> is a type expression ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_RELIMAGE_EQUAL_EMPTY}}||<math> r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset</math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_OVERL_EQUAL_EMPTY}}||<math>  r \ovl \cdots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \cdots \land s =  \emptyset </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_DPROD_EQUAL_EMPTY}}||<math>  p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_DPROD_EQUAL_TYPE}}||<math>  p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>\mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc})</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_PPROD_EQUAL_EMPTY}}||<math>  p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_PPROD_EQUAL_TYPE}}||<math>  p \pprod q = \mathit{Ty} \;\;\defi\;\;  p = \mathit{Ta} \cprod \mathit{Tc} \land q = \mathit{Tb} \cprod \mathit{Td} </math>|| where <math>\mathit{Ty}</math> is a type expression equal to <math>(\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td})</math> ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_ID_EQUAL_EMPTY}}||<math>  \id = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_PRJ1_EQUAL_EMPTY}}||<math>  \prjone = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 +
{{RRRow}}|||{{Rulename|SIMP_PRJ2_EQUAL_EMPTY}}||<math>  \prjtwo = \emptyset \;\;\defi\;\; \bfalse </math>||  ||  A
 +
|}
  
−
= Some identified difficulties =
 
  
−
== Initialization of elements from non UI components ==
+
[[Category:User documentation|The Proving Perspective]]
−
 
+
[[Category:Rodin Platform|The Proving Perspective]]
−
The following ElementDescRegistry method, shows the dependency between an element creation and the initialization of its attributes with default values.
+
[[Category:User manual|The Proving Perspective]]
−
 
 
−
        public <T extends IInternalElement> T createElement(
 
−
final IInternalElement root, IInternalElement parent,
 
−
final IInternalElementType<T> type, final IInternalElement sibling)
 
−
throws RodinDBException {
 
−
final T newElement = parent.createChild(type, sibling, null);
 
−
final IAttributeDesc[] attrDesc = getAttributes(type);
 
−
for (IAttributeDesc desc : attrDesc) {
 
−
desc.getManipulation().setDefaultValue(newElement, null);    // <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
 
−
}
 
−
return newElement;
 
−
}
 
−
 
 
−
The protocol shall be changed to take into account this initialization outside from the graphical manipulation.
 
−
Doing the initialization at org.eventb.core level is possible by registering a special "attribute initializer". <br>
 
−
WARNING : Only "choice" attributes can be marked as mandatory ({{ident|required}} attribute of the extension). Can't it be available for all kind of attributes?
 
−
 
 
−
== Correspondence between UI manipulation and "core" elements ==
 
−
If some element or attribute relationship is declared at the database level, but there is no corresponding {{ident|editorItem}} for it, it will be ignored by the UI. This is similar to the previous situation where some elements or attributes could be present in the database but not in the user interface hierarchy.
 
−
 
 
−
== Operation on elements shall be enforced ==
 
−
 
−
        private <T extends IInternalElement> OperationCreateElement getCreateElement(
 
−
IInternalElement parent, IInternalElementType<T> type,
 
−
IInternalElement sibling, IAttributeValue[] values) {
 
−
OperationCreateElement op = new OperationCreateElement(
 
−
createDefaultElement(parent, type, sibling));
 
−
op.addSubCommande(new ChangeAttribute(values));
 
−
return op;
 
−
}
 
−
 
 
−
''The Operation model similar to a kind of transaction mechanism, should be made available from the DB layer.''<br>
 
−
''The relations when using such layer shall be enforced and any invalid operation could be rejected.''
 
−
 
 
−
= Proposal =
 
−
 
 
−
== Hierarchy between elements ==
 
−
 
 
−
The part concerning element definition and hierarchy will go to a dedicated extension point in the database.
 
−
 
 
−
=== A - hierarchy definition ===
 
−
 
 
−
Here is the definition of the new extension point : org.rodinp.core.itemRelations which describes the possible children and attributes of internal elements.
 
−
 
 
−
Configuration Markup:
 
−
<!ELEMENT extension (relationship+)>
 
−
<!ATTLIST extension
 
−
point CDATA #REQUIRED
 
−
id    CDATA #IMPLIED
 
−
name  CDATA #IMPLIED
 
−
>
 
−
 
−
<!ELEMENT relationship ((childType | attributeType)+)>
 
−
<!ATTLIST elementRelationship
 
−
parentTypeId CDATA #REQUIRED
 
−
>
 
−
parentTypeId - Element type of the parent, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
−
 
−
<!ELEMENT childType EMPTY>
 
−
<!ATTLIST childType
 
−
typeId                CDATA #REQUIRED
 
−
>
 
−
typeId - Element type of the child, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
−
 
−
<!ELEMENT attributeType EMPTY>
 
−
<!ATTLIST attributeType
 
−
typeId CDATA #REQUIRED
 
−
>
 
−
attributeTypeId - Id of the Rodin attribute type to which this description applies (see extension point org.rodinp.core.attributeTypes).
 
−
 
−
The use of such extension point is obvious in org.eventb.core plug-in, as it would complement the extensions of org.rodinp.core.attributeTypes and org.rodinp.core.internalElementTypes.
 
−
 
 
−
=== B - API to declare and test the element/attribute relations and traverse them ===
 
−
 
 
−
The API of the Rodin database is extended as follows:
 
−
 
 
−
* interface IInternalElementType is extended with methods
 
−
 
 
−
  IInternalElementType<?>[] getParentTypes();
 
−
  IInternalElementType<?>[] getChildTypes();
 
−
  IAttributeType[] getAttributeTypes();
 
−
 
 
−
  boolean canParent(IInternalElementType<?> childType);
 
−
  boolean isElementOf(IAttributeType attrType);
 
−
 
 
−
* interface IAttributeType is extended with methods
 
−
 
 
−
  IInternalElementType<?>[] getElementTypes();
 
−
 
 
−
  boolean isAttributeOf(IInternalElementType<?> elementType);
 
−
 
 
−
This list might be later extended with new methods such as
 
−
{{ident|isAncestorOf}} if this proves useful.
 
−
 
 
−
 
 
−
 
 
−
== UI related information ==
 
−
The part concerning how to display elements and UI related info will stay in the editorItems extension point and shall point to an element definition and hierachy.<br>
 
−
Relationships will disappear from the editorItems extension point.
 
−
 
 
−
The interfaces are refactored to become the following :
 
−
 
 
−
''NB. IITemDesc disappears as it is cumbersome to provide such interface for a sole method getPrefix(). ''
 
−
 
 
−
public interface IUIElementDesc extends IItemDesc {
 
−
 
−
        public String getPrefix();
 
−
 
−
public String getChildrenSuffix();
 
−
 
−
public IImageProvider getImageProvider();
 
−
 
−
public IAttributeDesc atColumn(int i);
 
−
 
−
public int getDefaultColumn();
 
−
 
−
public boolean isSelectable(int i);
 
−
 
−
public String getAutoNamePrefix();
 
−
 
−
public IElementPrettyPrinter getPrettyPrinter();
 
−
 
−
}
 
−
 
 
−
public interface IUIAttributeDesc extends IItemDesc {
 
−
 
−
        public String getPrefix();
 
−
 
−
public String getSuffix();
 
−
 
−
public IEditComposite createWidget();
 
−
 
−
public boolean isHorizontalExpand();
 
−
 
−
}
 
−
 
 
−
 
 
−
=== D - Compatibility with the upgrade mechanism ===
 
−
 
 
−
Things start with the org.rodinp.core.conversion extension point.<br>
 
−
The modifications are done in XPATH  there is no incompatibility introduced here.
 
−
 
 
−
[[Category:Design_proposal]]
 

Revision as of 13:39, 24 May 2013

Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Rewrite_Rules.

All rewrite rules that match the pattern \textbf{P}=\emptyset are also applicable to predicates of the form \textbf{P}\subseteq\emptyset and \emptyset=\textbf{P}, as these predicates are equivalent. All rewrite rules that match the pattern \textbf{P}=\mathit{Ty} are also applicable to predicates of the form \mathit{Ty}\subseteq\textbf{P} and \mathit{Ty}=\textbf{P}, as these predicates are equivalent.


  Name Rule Side Condition A/M
*
DEF_SPECIAL_NOT_EQUAL
 \lnot\, S = \emptyset \;\;\defi\;\; \exists x \qdot x \in S where x is not free in S M
SIMP_SETENUM_EQUAL_EMPTY
 \{ A, \ldots , B\} = \emptyset \;\;\defi\;\; \bfalse A
*
SIMP_SPECIAL_EQUAL_COMPSET
 \{ x \qdot P(x) \mid E \} = \emptyset \;\;\defi\;\; \forall x\qdot \lnot\, P(x) A
SIMP_BINTER_EQUAL_TYPE
 A \binter \cdots \binter B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land \cdots \land B = \mathit{Ty} where \mathit{Ty} is a type expression A
SIMP_BINTER_SING_EQUAL_EMPTY
 A \binter \{ a \} = \emptyset \;\;\defi\;\; \lnot\, a \in A A
SIMP_BINTER_SETMINUS_EQUAL_EMPTY
 (A \setminus B) \binter C = \emptyset \;\;\defi\;\; (A \binter C) \setminus B = \emptyset A
SIMP_BUNION_EQUAL_EMPTY
 A \bunion \cdots \bunion B = \emptyset \;\;\defi\;\; A = \emptyset \land \cdots \land B = \emptyset A
SIMP_SETMINUS_EQUAL_EMPTY
 A \setminus B = \emptyset \;\;\defi\;\; A \subseteq B A
SIMP_SETMINUS_EQUAL_TYPE
 A \setminus B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ty} \land B = \emptyset where \mathit{Ty} is a type expression A
SIMP_POW_EQUAL_EMPTY
 \pow (S) = \emptyset \;\;\defi\;\; \bfalse A
SIMP_POW1_EQUAL_EMPTY
 \pown (S) = \emptyset \;\;\defi\;\; S = \emptyset A
SIMP_KINTER_EQUAL_TYPE
 \inter (S) = \mathit{Ty} \;\;\defi\;\; S = \{ \mathit{Ty} \} where \mathit{Ty} is a type expression A
SIMP_KUNION_EQUAL_EMPTY
 \union (S) = \emptyset \;\;\defi\;\; S \subseteq \{ \emptyset \} A
SIMP_QINTER_EQUAL_TYPE
 (\Inter x\qdot P(x) \mid E(x)) = \mathit{Ty} \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \mathit{Ty} where \mathit{Ty} is a type expression A
SIMP_QUNION_EQUAL_EMPTY
 (\Union x\qdot P(x) \mid E(x)) = \emptyset \;\;\defi\;\; \forall x\qdot P(x) \limp E(x) = \emptyset A
SIMP_NATURAL_EQUAL_EMPTY
 \nat = \emptyset \;\;\defi\;\; \bfalse A
SIMP_NATURAL1_EQUAL_EMPTY
 \natn = \emptyset \;\;\defi\;\; \bfalse A
*
SIMP_TYPE_EQUAL_EMPTY
 \mathit{Ty} = \emptyset \;\;\defi\;\; \bfalse where \mathit{Ty} is a type expression A
SIMP_CPROD_EQUAL_EMPTY
 S \cprod T = \emptyset \;\;\defi\;\; S = \emptyset \lor T = \emptyset A
SIMP_CPROD_EQUAL_TYPE
 S \cprod T = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land T = \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
SIMP_UPTO_EQUAL_EMPTY
 i \upto j = \emptyset \;\;\defi\;\; i > j A
SIMP_UPTO_EQUAL_INTEGER
 i \upto j = \intg \;\;\defi\;\; \bfalse A
SIMP_UPTO_EQUAL_NATURAL
 i \upto j = \nat \;\;\defi\;\; \bfalse A
SIMP_UPTO_EQUAL_NATURAL1
 i \upto j = \natn \;\;\defi\;\; \bfalse A
*
SIMP_SPECIAL_EQUAL_REL
 A \rel B = \emptyset \;\;\defi\;\; \bfalse idem for operators \pfun \pinj A
SIMP_TYPE_EQUAL_REL
 A \rel B = \mathit{Ty} \;\;\defi\;\; A = \mathit{Ta} \land B = \mathit{Tb} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
*
SIMP_SPECIAL_EQUAL_RELDOM
 A \trel B = \emptyset \;\;\defi\;\; \lnot\, A = \emptyset \land B = \emptyset idem for operator \tfun A
SIMP_TYPE_EQUAL_RELDOMRAN
 A \trel B = \mathit{Ty} \;\;\defi\;\; \bfalse where \mathit{Ty} is a type expression, idem for operator \srel, \strel, \tfun, \tinj, \psur, \tsur, \tbij A
SIMP_SREL_EQUAL_EMPTY
 A \srel B = \emptyset \;\;\defi\;\; A = \emptyset \land \lnot\,B = \emptyset A
SIMP_STREL_EQUAL_EMPTY
 A \strel B = \emptyset \;\;\defi\;\; (A = \emptyset \leqv \lnot\,B = \emptyset) A
SIMP_DOM_EQUAL_EMPTY
 \dom (r) = \emptyset \;\;\defi\;\; r = \emptyset A
SIMP_RAN_EQUAL_EMPTY
 \ran (r) = \emptyset \;\;\defi\;\; r = \emptyset A
SIMP_FCOMP_EQUAL_EMPTY
 p \fcomp q = \emptyset \;\;\defi\;\; \ran (p) \binter \dom (q) = \emptyset A
SIMP_BCOMP_EQUAL_EMPTY
 p \bcomp q = \emptyset \;\;\defi\;\; \ran (q) \binter \dom (p) = \emptyset A
SIMP_DOMRES_EQUAL_EMPTY
 S \domres r = \emptyset \;\;\defi\;\; \dom (r) \binter S = \emptyset A
SIMP_DOMRES_EQUAL_TYPE
 S \domres r = \mathit{Ty} \;\;\defi\;\; S = \mathit{Ta} \land r = \mathit{Ty} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
SIMP_DOMSUB_EQUAL_EMPTY
 S \domsub r = \emptyset \;\;\defi\;\; \dom (r) \subseteq S A
SIMP_DOMSUB_EQUAL_TYPE
 S \domsub r = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} where \mathit{Ty} is a type expression A
SIMP_RANRES_EQUAL_EMPTY
 r \ranres S = \emptyset \;\;\defi\;\; \ran (r) \binter S = \emptyset A
SIMP_RANRES_EQUAL_TYPE
 r \ranres S = \mathit{Ty} \;\;\defi\;\; S = \mathit{Tb} \land r = \mathit{Ty} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod \mathit{Tb} A
SIMP_RANSUB_EQUAL_EMPTY
 r \ransub S = \emptyset \;\;\defi\;\; \ran (r) \subseteq S A
SIMP_RANSUB_EQUAL_TYPE
 r \ransub S = \mathit{Ty} \;\;\defi\;\; S = \emptyset \land r = \mathit{Ty} where \mathit{Ty} is a type expression A
SIMP_CONVERSE_EQUAL_EMPTY
 r^{-1} = \emptyset \;\;\defi\;\; r = \emptyset A
SIMP_CONVERSE_EQUAL_TYPE
 r^{-1} = \mathit{Ty} \;\;\defi\;\; r = \mathit{Ty}^{-1} where \mathit{Ty} is a type expression A
SIMP_RELIMAGE_EQUAL_EMPTY
 r[S] = \emptyset \;\;\defi\;\; S \domres r = \emptyset A
SIMP_OVERL_EQUAL_EMPTY
 r \ovl \cdots \ovl s = \emptyset \;\;\defi\;\; r = \emptyset \land \cdots \land s = \emptyset A
SIMP_DPROD_EQUAL_EMPTY
 p \dprod q = \emptyset \;\;\defi\;\; \dom (p) \binter \dom (q) = \emptyset A
SIMP_DPROD_EQUAL_TYPE
 p \dprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tb} \land q = \mathit{Ta} \cprod \mathit{Tc} where \mathit{Ty} is a type expression equal to \mathit{Ta} \cprod (\mathit{Tb} \cprod \mathit{Tc}) A
SIMP_PPROD_EQUAL_EMPTY
 p \pprod q = \emptyset \;\;\defi\;\; p = \emptyset \lor q = \emptyset A
SIMP_PPROD_EQUAL_TYPE
 p \pprod q = \mathit{Ty} \;\;\defi\;\; p = \mathit{Ta} \cprod \mathit{Tc} \land q = \mathit{Tb} \cprod \mathit{Td} where \mathit{Ty} is a type expression equal to (\mathit{Ta} \cprod \mathit{Tb}) \cprod (\mathit{Tc} \cprod \mathit{Td}) A
SIMP_ID_EQUAL_EMPTY
 \id = \emptyset \;\;\defi\;\; \bfalse A
SIMP_PRJ1_EQUAL_EMPTY
 \prjone = \emptyset \;\;\defi\;\; \bfalse A
SIMP_PRJ2_EQUAL_EMPTY
 \prjtwo = \emptyset \;\;\defi\;\; \bfalse A
Retrieved from ‘https://wiki.event-b.org/index.php?title=Element_Hierarchy_Extension_Point_%26_Library&oldid=4036’