Relation Rewrite Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Billaude Adding 9 new rewriting rules. |
imported>Billaude The four last rules already exist, but were not implemented. Instead of being manual, they are automatic. |
||
Line 129: | Line 129: | ||
{{RRRow}}|*||{{Rulename|SIMP_MULTI_DOM_CPROD}}||<math> \dom (E \cprod E) \;\;\defi\;\; E </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|SIMP_MULTI_RAN_CPROD}}||<math> \ran (E \cprod E) \;\;\defi\;\; E </math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_MULTI_DOM_DOMRES}}||<math>\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A</math>|| || | {{RRRow}}|*||{{Rulename|SIMP_MULTI_DOM_DOMRES}}||<math>\dom(A\domres f) \;\;\defi\;\; \dom(f)\binter A</math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_MULTI_DOM_DOMSUB}}||<math>\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A</math>|| || | {{RRRow}}|*||{{Rulename|SIMP_MULTI_DOM_DOMSUB}}||<math>\dom(A\domsub f) \;\;\defi\;\; \dom(f)\setminus A</math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_MULTI_RAN_RANRES}}||<math>\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A</math>|| || | {{RRRow}}|*||{{Rulename|SIMP_MULTI_RAN_RANRES}}||<math>\ran(f\ranres A) \;\;\defi\;\; \ran(f)\binter A</math>|| || A | ||
{{RRRow}}| ||{{Rulename|SIMP_MULTI_RAN_RANSUB}}||<math>\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A</math>|| || | {{RRRow}}|*||{{Rulename|SIMP_MULTI_RAN_RANSUB}}||<math>\ran(f\ransub A) \;\;\defi\;\; \ran(f)\setminus A</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_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_RAN}}||<math> F \in \ran (r) \;\;\defi\;\; \exists x \qdot x \mapsto F \in r </math>|| || M | ||
Line 219: | Line 219: | ||
{{RRRow}}|*||{{Rulename|DERIV_MULTI_IN_SETMINUS}}||<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> || || A | {{RRRow}}|*||{{Rulename|DERIV_MULTI_IN_SETMINUS}}||<math> E\in S\setminus\left\{\cdots, E,\cdots\right\} \;\;\defi\;\; \bfalse</math> || || A | ||
{{RRRow}}|*||{{Rulename|DEF_PRED}}||<math> \upred\;\;\defi\;\; \usucc^{-1}</math> || || A | {{RRRow}}|*||{{Rulename|DEF_PRED}}||<math> \upred\;\;\defi\;\; \usucc^{-1}</math> || || A | ||
|} | |} |
Revision as of 12:48, 30 September 2011
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.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | SIMP_DOM_SETENUM |
A | ||
* | SIMP_DOM_CONVERSE |
A | ||
* | SIMP_RAN_SETENUM |
A | ||
* | SIMP_RAN_CONVERSE |
A | ||
* | SIMP_SPECIAL_OVERL |
A | ||
* | SIMP_MULTI_OVERL |
there is a such that and and are syntactically equal. | A | |
* | SIMP_TYPE_OVERL_CPROD |
where is a type expression | A | |
* | SIMP_SPECIAL_DOMRES_L |
A | ||
* | SIMP_SPECIAL_DOMRES_R |
A | ||
* | SIMP_TYPE_DOMRES |
where is a type expression | A | |
* | SIMP_MULTI_DOMRES_DOM |
A | ||
* | SIMP_MULTI_DOMRES_RAN |
A | ||
* | SIMP_DOMRES_DOMRES_ID |
A | ||
* | SIMP_DOMRES_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_RANRES_R |
A | ||
* | SIMP_SPECIAL_RANRES_L |
A | ||
* | SIMP_TYPE_RANRES |
where is a type expression | A | |
* | SIMP_MULTI_RANRES_RAN |
A | ||
* | SIMP_MULTI_RANRES_DOM |
A | ||
* | SIMP_RANRES_ID |
A | ||
* | SIMP_RANSUB_ID |
A | ||
* | SIMP_RANRES_DOMRES_ID |
A | ||
* | SIMP_RANRES_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_DOMSUB_L |
A | ||
* | SIMP_SPECIAL_DOMSUB_R |
A | ||
* | SIMP_TYPE_DOMSUB |
where is a type expression | A | |
* | SIMP_MULTI_DOMSUB_DOM |
A | ||
* | SIMP_MULTI_DOMSUB_RAN |
A | ||
* | SIMP_DOMSUB_DOMRES_ID |
A | ||
* | SIMP_DOMSUB_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_RANSUB_R |
A | ||
* | SIMP_SPECIAL_RANSUB_L |
A | ||
* | SIMP_TYPE_RANSUB |
where is a type expression | A | |
* | SIMP_MULTI_RANSUB_DOM |
A | ||
* | SIMP_MULTI_RANSUB_RAN |
A | ||
* | SIMP_RANSUB_DOMRES_ID |
A | ||
* | SIMP_RANSUB_DOMSUB_ID |
A | ||
* | SIMP_SPECIAL_FCOMP |
A | ||
* | SIMP_TYPE_FCOMP_ID |
A | ||
* | SIMP_TYPE_FCOMP_R |
where is a type expression equal to | A | |
* | SIMP_TYPE_FCOMP_L |
where is a type expression equal to | A | |
* | SIMP_FCOMP_ID |
A | ||
* | SIMP_SPECIAL_BCOMP |
A | ||
* | SIMP_TYPE_BCOMP_ID |
A | ||
* | SIMP_TYPE_BCOMP_L |
where is a type expression equal to | A | |
* | SIMP_TYPE_BCOMP_R |
where is a type expression equal to | A | |
* | SIMP_BCOMP_ID |
A | ||
* | SIMP_SPECIAL_DPROD_R |
A | ||
* | SIMP_SPECIAL_DPROD_L |
A | ||
* | SIMP_DPROD_CPROD |
A | ||
* | SIMP_SPECIAL_PPROD_R |
A | ||
* | SIMP_SPECIAL_PPROD_L |
A | ||
* | SIMP_PPROD_CPROD |
A | ||
* | SIMP_SPECIAL_RELIMAGE_R |
A | ||
* | SIMP_SPECIAL_RELIMAGE_L |
A | ||
* | SIMP_TYPE_RELIMAGE |
where is a type expression | A | |
* | SIMP_MULTI_RELIMAGE_DOM |
A | ||
* | SIMP_RELIMAGE_ID |
A | ||
* | SIMP_RELIMAGE_DOMRES_ID |
A | ||
* | SIMP_RELIMAGE_DOMSUB_ID |
A | ||
* | SIMP_MULTI_RELIMAGE_CPROD_SING |
where is a single expression | A | |
* | SIMP_MULTI_RELIMAGE_SING_MAPSTO |
where is a single expression | A | |
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB |
A | ||
* | SIMP_MULTI_RELIMAGE_CONVERSE_RANRES |
A | ||
* | SIMP_RELIMAGE_CONVERSE_DOMSUB |
A | ||
DERIV_RELIMAGE_RANSUB |
M | |||
DERIV_RELIMAGE_RANRES |
M | |||
* | SIMP_MULTI_RELIMAGE_DOMSUB |
A | ||
DERIV_RELIMAGE_DOMSUB |
M | |||
DERIV_RELIMAGE_DOMRES |
M | |||
* | SIMP_SPECIAL_CONVERSE |
A | ||
* | SIMP_CONVERSE_ID |
A | ||
* | SIMP_CONVERSE_CPROD |
A | ||
* | SIMP_CONVERSE_SETENUM |
A | ||
* | SIMP_CONVERSE_COMPSET |
A | ||
* | SIMP_DOM_ID |
where has type | A | |
* | SIMP_RAN_ID |
where has type | A | |
* | SIMP_FCOMP_ID_L |
A | ||
* | SIMP_FCOMP_ID_R |
A | ||
* | SIMP_SPECIAL_REL_R |
idem for operators | A | |
* | SIMP_SPECIAL_REL_L |
idem for operators | A | |
* | SIMP_SPECIAL_EQUAL_REL |
idem for operators | A | |
* | SIMP_SPECIAL_EQUAL_RELDOM |
idem for operators | A | |
* | SIMP_FUNIMAGE_PRJ1 |
A | ||
* | SIMP_FUNIMAGE_PRJ2 |
A | ||
* | SIMP_DOM_PRJ1 |
where has type | A | |
* | SIMP_DOM_PRJ2 |
where has type | A | |
* | SIMP_RAN_PRJ1 |
where has type | A | |
* | SIMP_RAN_PRJ2 |
where has type | A | |
* | SIMP_FUNIMAGE_LAMBDA |
A | ||
* | SIMP_DOM_LAMBDA |
A | ||
* | SIMP_RAN_LAMBDA |
A | ||
* | SIMP_IN_FUNIMAGE |
A | ||
* | SIMP_IN_FUNIMAGE_CONVERSE_L |
A | ||
* | SIMP_IN_FUNIMAGE_CONVERSE_R |
A | ||
* | SIMP_MULTI_FUNIMAGE_SETENUM_LL |
A | ||
* | SIMP_MULTI_FUNIMAGE_SETENUM_LR |
A | ||
* | SIMP_MULTI_FUNIMAGE_OVERL_SETENUM |
A | ||
* | SIMP_MULTI_FUNIMAGE_BUNION_SETENUM |
A | ||
* | SIMP_FUNIMAGE_CPROD |
A | ||
* | SIMP_FUNIMAGE_ID |
A | ||
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE |
A | ||
* | SIMP_FUNIMAGE_CONVERSE_FUNIMAGE |
A | ||
* | SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM |
A | ||
* | SIMP_FUNIMAGE_DOMRES |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_DOMSUB |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_RANRES |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_RANSUB |
with hypothesis where is one of , , , , , , . | AM | |
* | SIMP_FUNIMAGE_SETMINUS |
with hypothesis where is one of , , , , , , . | AM | |
DEF_BCOMP |
M | |||
DERIV_ID_SING |
where is a single expression | M | ||
* | SIMP_SPECIAL_DOM |
A | ||
* | SIMP_SPECIAL_RAN |
A | ||
* | SIMP_CONVERSE_CONVERSE |
A | ||
* | DERIV_RELIMAGE_FCOMP |
M | ||
* | DERIV_FCOMP_DOMRES |
M | ||
* | DERIV_FCOMP_DOMSUB |
M | ||
* | DERIV_FCOMP_RANRES |
M | ||
* | DERIV_FCOMP_RANSUB |
M | ||
DERIV_FCOMP_SING |
A | |||
* | SIMP_SPECIAL_EQUAL_RELDOMRAN |
idem for operators | A | |
* | SIMP_TYPE_DOM |
where is a type expression equal to | A | |
* | SIMP_TYPE_RAN |
where is a type expression equal to | A | |
* | SIMP_MULTI_DOM_CPROD |
A | ||
* | SIMP_MULTI_RAN_CPROD |
A | ||
* | SIMP_MULTI_DOM_DOMRES |
A | ||
* | SIMP_MULTI_DOM_DOMSUB |
A | ||
* | SIMP_MULTI_RAN_RANRES |
A | ||
* | SIMP_MULTI_RAN_RANSUB |
A | ||
* | DEF_IN_DOM |
M | ||
* | DEF_IN_RAN |
M | ||
* | DEF_IN_CONVERSE |
M | ||
* | DEF_IN_DOMRES |
M | ||
* | DEF_IN_RANRES |
M | ||
* | DEF_IN_DOMSUB |
M | ||
* | DEF_IN_RANSUB |
M | ||
* | DEF_IN_RELIMAGE |
M | ||
* | DEF_IN_FCOMP |
M | ||
* | DEF_OVERL |
M | ||
* | DEF_IN_ID |
M | ||
* | DEF_IN_DPROD |
M | ||
* | DEF_IN_PPROD |
M | ||
* | DEF_IN_REL |
M | ||
* | DEF_IN_RELDOM |
M | ||
* | DEF_IN_RELRAN |
M | ||
* | DEF_IN_RELDOMRAN |
M | ||
* | DEF_IN_FCT |
M | ||
* | DEF_IN_TFCT |
M | ||
* | DEF_IN_INJ |
M | ||
* | DEF_IN_TINJ |
M | ||
* | DEF_IN_SURJ |
M | ||
* | DEF_IN_TSURJ |
M | ||
* | DEF_IN_BIJ |
M | ||
DISTRI_BCOMP_BUNION |
M | |||
* | DISTRI_FCOMP_BUNION_R |
M | ||
* | DISTRI_FCOMP_BUNION_L |
M | ||
DISTRI_DPROD_BUNION |
M | |||
DISTRI_DPROD_BINTER |
M | |||
DISTRI_DPROD_SETMINUS |
M | |||
DISTRI_DPROD_OVERL |
M | |||
DISTRI_PPROD_BUNION |
M | |||
DISTRI_PPROD_BINTER |
M | |||
DISTRI_PPROD_SETMINUS |
M | |||
DISTRI_PPROD_OVERL |
M | |||
DISTRI_OVERL_BUNION_L |
M | |||
DISTRI_OVERL_BINTER_L |
M | |||
* | DISTRI_DOMRES_BUNION_R |
M | ||
* | DISTRI_DOMRES_BUNION_L |
M | ||
* | DISTRI_DOMRES_BINTER_R |
M | ||
* | DISTRI_DOMRES_BINTER_L |
M | ||
DISTRI_DOMRES_SETMINUS_R |
M | |||
DISTRI_DOMRES_SETMINUS_L |
M | |||
DISTRI_DOMRES_DPROD |
M | |||
DISTRI_DOMRES_OVERL |
M | |||
* | DISTRI_DOMSUB_BUNION_R |
M | ||
* | DISTRI_DOMSUB_BUNION_L |
M | ||
* | DISTRI_DOMSUB_BINTER_R |
M | ||
* | DISTRI_DOMSUB_BINTER_L |
M | ||
DISTRI_DOMSUB_DPROD |
M | |||
DISTRI_DOMSUB_OVERL |
M | |||
* | DISTRI_RANRES_BUNION_R |
M | ||
* | DISTRI_RANRES_BUNION_L |
M | ||
* | DISTRI_RANRES_BINTER_R |
M | ||
* | DISTRI_RANRES_BINTER_L |
M | ||
DISTRI_RANRES_SETMINUS_R |
M | |||
DISTRI_RANRES_SETMINUS_L |
M | |||
* | DISTRI_RANSUB_BUNION_R |
M | ||
* | DISTRI_RANSUB_BUNION_L |
M | ||
* | DISTRI_RANSUB_BINTER_R |
M | ||
* | DISTRI_RANSUB_BINTER_L |
M | ||
* | DISTRI_CONVERSE_BUNION |
M | ||
DISTRI_CONVERSE_BINTER |
M | |||
DISTRI_CONVERSE_SETMINUS |
M | |||
DISTRI_CONVERSE_BCOMP |
M | |||
DISTRI_CONVERSE_FCOMP |
M | |||
DISTRI_CONVERSE_PPROD |
M | |||
DISTRI_CONVERSE_DOMRES |
M | |||
DISTRI_CONVERSE_DOMSUB |
M | |||
DISTRI_CONVERSE_RANRES |
M | |||
DISTRI_CONVERSE_RANSUB |
M | |||
* | DISTRI_DOM_BUNION |
M | ||
* | DISTRI_RAN_BUNION |
M | ||
* | DISTRI_RELIMAGE_BUNION_R |
M | ||
* | DISTRI_RELIMAGE_BUNION_L |
M | ||
* | DERIV_DOM_TOTALREL |
with hypothesis , where is one of | M | |
DERIV_RAN_SURJREL |
with hypothesis , where is one of | M | ||
b | prjone-functional |
where is one of | A | |
b | prjtwo-functional |
where is one of | A | |
prj-expand |
M | |||
* | SIMP_DOM_SUCC |
A | ||
* | SIMP_RAN_SUCC |
A | ||
* | DERIV_MULTI_IN_BUNION |
A | ||
* | DERIV_MULTI_IN_SETMINUS |
A | ||
* | DEF_PRED |
A |