Empty Set Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Josselin Fixed side condition (SIMP_TYPE_EQUAL_RELDOMRAN) |
imported>Josselin Fixed rule SIMP_PPROD_EQUAL_TYPE (the condition did not typecheck) |
||
Line 53: | Line 53: | ||
{{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_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_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{ | {{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_ID_EQUAL_EMPTY}}||<math> \id = \emptyset \;\;\defi\;\; \bfalse </math>|| || A | ||
{{RRRow}}|||{{Rulename|SIMP_PRJ1_EQUAL_EMPTY}}||<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>|| || A | {{RRRow}}|||{{Rulename|SIMP_PRJ1_EQUAL_EMPTY}}||<math> \prjone = \emptyset \;\;\defi\;\; \bfalse </math>|| || A |
Revision as of 08:14, 22 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 are also applicable to predicates of the form and , as these predicates are equivalent.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | DEF_SPECIAL_NOT_EQUAL |
where is not free in | M | |
SIMP_SETENUM_EQUAL_EMPTY |
A | |||
* | SIMP_SPECIAL_EQUAL_COMPSET |
A | ||
SIMP_BINTER_EQUAL_TYPE |
where is a type expression | A | ||
SIMP_BUNION_EQUAL_EMPTY |
A | |||
SIMP_SETMINUS_EQUAL_EMPTY |
A | |||
SIMP_SETMINUS_EQUAL_TYPE |
where is a type expression | A | ||
SIMP_POW_EQUAL_EMPTY |
A | |||
SIMP_POW1_EQUAL_EMPTY |
A | |||
SIMP_KINTER_EQUAL_TYPE |
where is a type expression | A | ||
SIMP_KUNION_EQUAL_EMPTY |
A | |||
SIMP_QINTER_EQUAL_TYPE |
where is a type expression | A | ||
SIMP_QUNION_EQUAL_EMPTY |
A | |||
SIMP_NATURAL_EQUAL_EMPTY |
A | |||
SIMP_NATURAL1_EQUAL_EMPTY |
A | |||
* | SIMP_TYPE_EQUAL_EMPTY |
where is a type expression | A | |
SIMP_CPROD_EQUAL_EMPTY |
A | |||
SIMP_CPROD_EQUAL_TYPE |
where is a type expression equal to | A | ||
SIMP_UPTO_EQUAL_EMPTY |
A | |||
SIMP_UPTO_EQUAL_INTEGER |
A | |||
SIMP_UPTO_EQUAL_NATURAL |
A | |||
SIMP_UPTO_EQUAL_NATURAL1 |
A | |||
* | SIMP_SPECIAL_EQUAL_REL |
idem for operators | A | |
SIMP_TYPE_EQUAL_REL |
where is a type expression equal to | A | ||
* | SIMP_SPECIAL_EQUAL_RELDOM |
idem for operator | A | |
SIMP_TYPE_EQUAL_RELDOMRAN |
where is a type expression, idem for operator | A | ||
SIMP_SREL_EQUAL_EMPTY |
A | |||
SIMP_STREL_EQUAL_EMPTY |
A | |||
SIMP_DOM_EQUAL_EMPTY |
A | |||
SIMP_RAN_EQUAL_EMPTY |
A | |||
SIMP_FCOMP_EQUAL_EMPTY |
A | |||
SIMP_BCOMP_EQUAL_EMPTY |
A | |||
SIMP_DOMRES_EQUAL_EMPTY |
A | |||
SIMP_DOMRES_EQUAL_TYPE |
where is a type expression equal to | A | ||
SIMP_DOMSUB_EQUAL_EMPTY |
A | |||
SIMP_DOMSUB_EQUAL_TYPE |
where is a type expression | A | ||
SIMP_RANRES_EQUAL_EMPTY |
A | |||
SIMP_RANRES_EQUAL_TYPE |
where is a type expression equal to | A | ||
SIMP_RANSUB_EQUAL_EMPTY |
A | |||
SIMP_RANSUB_EQUAL_TYPE |
where is a type expression | A | ||
SIMP_CONVERSE_EQUAL_EMPTY |
A | |||
SIMP_CONVERSE_EQUAL_TYPE |
where is a type expression | A | ||
SIMP_RELIMAGE_EQUAL_EMPTY |
A | |||
SIMP_OVERL_EQUAL_EMPTY |
A | |||
SIMP_DPROD_EQUAL_EMPTY |
A | |||
SIMP_DPROD_EQUAL_TYPE |
where is a type expression equal to | A | ||
SIMP_PPROD_EQUAL_EMPTY |
A | |||
SIMP_PPROD_EQUAL_TYPE |
where is a type expression equal to | A | ||
SIMP_ID_EQUAL_EMPTY |
A | |||
SIMP_PRJ1_EQUAL_EMPTY |
A | |||
SIMP_PRJ1_EQUAL_TYPE |
where is a type expression equal to | A | ||
SIMP_PRJ2_EQUAL_EMPTY |
A | |||
SIMP_PRJ2_EQUAL_TYPE |
where is a type expression equal to | A |