# Difference between revisions of "Inference Rules"

From Event-B

Jump to navigationJump to searchimported>Laurent (Added rule IMP_CASE) |
imported>Laurent (Added rules FIN_REL, FIN_FUN_DOM and FIN_FUN_RAN) |
||

Line 144: | Line 144: | ||

{{RRRow}}|*||{{Rulename|FIN_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash | {{RRRow}}|*||{{Rulename|FIN_SETMINUS_R}}|| <math>\frac{\textbf{H} \;\;\vdash | ||

\;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> || || M | \;\;\finite\,(S)}{\textbf{H} \;\;\vdash \;\; \finite\,(S \;\setminus\; T)}</math> || || M | ||

+ | |||

+ | {{RRRow}}|*||{{Rulename|FIN_REL}}|| <math>\frac{}{\textbf{H},\; r\in S\;\mathit{op}\;T,\; \finite\,(S),\; \finite\,(T) \;\;\vdash \;\; \finite\,(r)}</math> || where <math>\mathit{op}</math> denotes a set of relations (any arrow) || A | ||

{{RRRow}}|*||{{Rulename|FIN_REL_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\rel T) \qquad\textbf{H} \;\;\vdash \;\; r \;\in\; S \rel T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(r)}</math> || the user has to write the set corresponding to <math>S \rel T</math> in the editing area of the Proof Control Window || M | {{RRRow}}|*||{{Rulename|FIN_REL_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\rel T) \qquad\textbf{H} \;\;\vdash \;\; r \;\in\; S \rel T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) \qquad \textbf{H} \;\;\vdash \;\; \finite\,(T)}{\textbf{H} \;\;\vdash \;\; \finite\,(r)}</math> || the user has to write the set corresponding to <math>S \rel T</math> in the editing area of the Proof Control Window || M | ||

Line 152: | Line 154: | ||

{{RRRow}}|*||{{Rulename|FIN_REL_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r))}</math> || || M | {{RRRow}}|*||{{Rulename|FIN_REL_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite\,(r) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(r))}</math> || || M | ||

+ | |||

+ | {{RRRow}}|*||{{Rulename|FIN_FUN_DOM}}|| <math>\frac{}{\textbf{H},\; f\in S\;\mathit{op}\;T,\; \finite\,(S) \;\;\vdash \;\; \finite\,(f)}</math> || where <math>\mathit{op}</math> is one of <math>\pfun</math>, <math>\tfun</math>, <math>\pinj</math>, <math>\tinj</math>, <math>\psur</math>, <math>\tsur</math>, <math>\tbij</math> || A | ||

+ | |||

+ | {{RRRow}}|*||{{Rulename|FIN_FUN_RAN}}|| <math>\frac{}{\textbf{H},\; f\in S\;\mathit{op}\;T,\; \finite\,(T) \;\;\vdash \;\; \finite\,(f)}</math> || where <math>\mathit{op}</math> is one of <math>\pinj</math>, <math>\tinj</math>, <math>\tbij</math> || A | ||

{{RRRow}}|*||{{Rulename|FIN_FUN1_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f)}</math> || the user has to write the set corresponding to <math>S \pfun T</math> in the editing area of the Proof Control Window || M | {{RRRow}}|*||{{Rulename|FIN_FUN1_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(f)}</math> || the user has to write the set corresponding to <math>S \pfun T</math> in the editing area of the Proof Control Window || M |

## Revision as of 16:44, 4 April 2011

CAUTION! Any modification to this page shall be announced on the User mailing list!

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)#Inference_Rules.

Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|

* | HYP |
A
| ||

* | HYP_OR |
A
| ||

* | CNTR |
A
| ||

* | FALSE_HYP |
A
| ||

* | TRUE_GOAL |
A
| ||

* | FUN_GOAL |
where and denote types and is one of , , , , , , . | A
| |

* | FUN_IMAGE_GOAL |
where denotes a set of relations (any arrow) and is WD strict | M
| |

FUN_GOAL_REC |
where and denote types, denotes a set of relations (any arrow) and is one of , , , , , , . | A
| ||

* | DBL_HYP |
A
| ||

* | AND_L |
A
| ||

* | AND_R |
A
| ||

IMP_L1 |
A
| |||

* | IMP_R |
A
| ||

* | IMP_AND_L |
A
| ||

* | IMP_OR_L |
A
| ||

* | AUTO_MH |
A
| ||

* | NEG_IN_L |
A
| ||

* | NEG_IN_R |
A
| ||

* | XST_L |
A
| ||

* | ALL_R |
A
| ||

* | EQL_LR |
is a variable which is not free in | A
| |

* | EQL_RL |
is a variable which is not free in | A
| |

SUBSET_INTER |
where and are not bound by | A
| ||

IN_INTER |
where and are not bound by | A
| ||

NOTIN_INTER |
where and are not bound by | A
| ||

* | FIN_L_LOWER_BOUND_L |
The goal is discharged | A
| |

* | FIN_L_LOWER_BOUND_R |
The goal is discharged | A
| |

* | FIN_L_UPPER_BOUND_L |
The goal is discharged | A
| |

* | FIN_L_UPPER_BOUND_R |
The goal is discharged | A
| |

* | CONTRADICT_L |
M
| ||

* | CONTRADICT_R |
M
| ||

* | CASE |
M
| ||

IMP_CASE |
M
| |||

* | MH |
M
| ||

* | HM |
M
| ||

EQV |
M
| |||

* | OV_SETENUM_L |
where is WD strict | A
| |

* | OV_SETENUM_R |
where is WD strict | A
| |

* | OV_L |
where is WD strict | A
| |

* | OV_R |
where is WD strict | A
| |

* | DIS_BINTER_R |
where is WD strict, and denote types. | M
| |

* | DIS_BINTER_L |
where is WD strict, and denote types. | M
| |

* | DIS_SETMINUS_R |
where is WD strict, and denote types. | M
| |

* | DIS_SETMINUS_L |
where is WD strict, and denote types. | M
| |

* | SIM_REL_IMAGE_R |
M
| ||

* | SIM_REL_IMAGE_L |
M
| ||

* | SIM_FCOMP_R |
M
| ||

* | SIM_FCOMP_L |
M
| ||

* | FIN_SUBSETEQ_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |

* | FIN_BINTER_R |
M
| ||

FIN_KINTER_R |
where is fresh | M
| ||

FIN_QINTER_R |
M
| |||

* | FIN_SETMINUS_R |
M
| ||

* | FIN_REL |
where denotes a set of relations (any arrow) | A
| |

* | FIN_REL_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |

* | FIN_REL_IMG_R |
M
| ||

* | FIN_REL_RAN_R |
M
| ||

* | FIN_REL_DOM_R |
M
| ||

* | FIN_FUN_DOM |
where is one of , , , , , , | A
| |

* | FIN_FUN_RAN |
where is one of , , | A
| |

* | FIN_FUN1_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |

* | FIN_FUN2_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |

* | FIN_FUN_IMG_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |

* | FIN_FUN_RAN_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |

* | FIN_FUN_DOM_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |

* | LOWER_BOUND_L |
must not contain any bound variable | M
| |

* | LOWER_BOUND_R |
must not contain any bound variable | M
| |

* | UPPER_BOUND_L |
must not contain any bound variable | M
| |

* | UPPER_BOUND_R |
must not contain any bound variable | M
| |

* | FIN_LT_0 |
M
| ||

* | FIN_GE_0 |
M
| ||

CARD_INTERV |
where is WD strict | M
| ||

CARD_EMPTY_INTERV |
where is WD strict | M
| ||

* | DERIV_LE_CARD |
and bear the same type | M
| |

* | DERIV_GE_CARD |
and bear the same type | M
| |

* | DERIV_LT_CARD |
and bear the same type | M
| |

* | DERIV_GT_CARD |
and bear the same type | M
| |

* | DERIV_EQUAL_CARD |
and bear the same type | M
| |

SIMP_CARD_SETMINUS_L |
where is WD strict | M | ||

SIMP_CARD_SETMINUS_R |
where is WD strict | M
| ||

SIMP_CARD_CPROD_L |
where is WD strict | M | ||

SIMP_CARD_CPROD_R |
where is WD strict | M
| ||

* | FORALL_INST |
is instantiated with | M
| |

* | FORALL_INST_MP |
is instantiated with and a Modus Ponens is applied | M
| |

* | FORALL_INST_MT |
is instantiated with and a Modus Tollens is applied | M
| |

* | CUT |
hypothesis is added | M
| |

* | EXISTS_INST |
is instantiated with | M
| |

* | DISTINCT_CASE |
case distinction on predicate | M
| |

* | ONE_POINT_L |
The rule can be applied with as well as with | A
| |

* | ONE_POINT_R |
The rule can be applied with as well as with | A |

See also Extension Proof Rules#Inference Rules.