Difference between revisions of "Inference Rules"
From Event-B
Jump to navigationJump to searchimported>Laurent (Replaced CARD_SUBSETEQ by DERIV_LE_CARD, DERIV_GE_CARD, DERIV_LT_CARD, DERIV_GT_CARD, DERIV_EQUAL_CARD.) |
imported>Tommy m (Mark FIN_FUN_* as fixed(*). Fixed in r8042.) |
||
Line 134: | Line 134: | ||
{{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}}| | + | {{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}}| | + | {{RRRow}}|*||{{Rulename|FIN_FUN2_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f^{-1} \;\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}}| | + | {{RRRow}}|*||{{Rulename|FIN_FUN_IMG_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[s])}</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}}| | + | {{RRRow}}|*||{{Rulename|FIN_FUN_RAN_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\,(\ran(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}}| | + | {{RRRow}}|*||{{Rulename|FIN_FUN_DOM_R}}|| <math>\frac{\textbf{H} \;\;\vdash\;\;{WD}(S\pfun T) \qquad\textbf{H} \;\;\vdash \;\; f^{-1} \;\in\; S \pfun T \qquad \textbf{H} \;\;\vdash \;\; \finite\,(S) }{\textbf{H} \;\;\vdash \;\; \finite\,(\dom(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|LOWER_BOUND_L}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S) }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}</math> || <math>S</math> must not contain any bound variable || M | {{RRRow}}|*||{{Rulename|LOWER_BOUND_L}}|| <math>\frac{\textbf{H} \;\;\vdash \;\; \finite(S) }{\textbf{H} \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}</math> || <math>S</math> must not contain any bound variable || M |
Revision as of 15:43, 13 January 2010
Conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Inference_Rules.
Rules that are marked with a b in the first column are currently broken in Rodin 1.1 (see bug 2895507).
Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|
* | HYP |
![]() |
A
| |
* | HYP_OR |
![]() |
A
| |
* | CNTR |
![]() |
A
| |
* | FALSE_HYP |
![]() |
A
| |
* | TRUE_GOAL |
![]() |
A
| |
* | FUN_GOAL |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |
![]() |
![]() ![]() |
A
|
* | EQL_RL |
![]() |
![]() ![]() |
A
|
SUBSET_INTER |
![]() |
the ![]() |
A
| |
IN_INTER |
![]() |
the ![]() |
A
| |
NOTIN_INTER |
![]() |
the ![]() |
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
| |
* | MH |
![]() |
M
| |
* | HM |
![]() |
M
| |
EQV |
![]() |
M
| ||
* | OV_L |
![]() |
the ![]() |
M
|
* | OV_R |
![]() |
the ![]() |
M
|
* | OV_L |
![]() |
the ![]() |
M
|
* | OV_R |
![]() |
the ![]() |
M
|
* | DIS_BINTER_R |
![]() |
the occurrence of ![]() ![]() ![]() |
M
|
* | DIS_BINTER_L |
![]() |
the occurrence of ![]() ![]() ![]() |
M
|
* | DIS_SETMINUS_R |
![]() |
the occurrence of ![]() ![]() ![]() |
M
|
* | DIS_SETMINUS_L |
![]() |
the occurrence of ![]() ![]() ![]() |
M
|
* | SIM_REL_IMAGE_R |
![]() |
the occurrence of ![]() |
M
|
* | SIM_REL_IMAGE_L |
![]() |
the occurrence of ![]() |
M
|
* | SIM_FCOMP_R |
![]() |
the occurrence of ![]() |
M
|
* | SIM_FCOMP_L |
![]() |
the occurrence of ![]() |
M
|
* | FIN_SUBSETEQ_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_BINTER_R |
![]() |
M
| |
* | FIN_SETMINUS_R |
![]() |
M
| |
* | FIN_REL_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_REL_IMG_R |
![]() |
M
| |
* | FIN_REL_RAN_R |
![]() |
M
| |
* | FIN_REL_DOM_R |
![]() |
M
| |
* | FIN_FUN1_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN2_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_IMG_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_RAN_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_DOM_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | LOWER_BOUND_L |
![]() |
![]() |
M
|
* | LOWER_BOUND_R |
![]() |
![]() |
M
|
* | UPPER_BOUND_L |
![]() |
![]() |
M
|
* | UPPER_BOUND_R |
![]() |
![]() |
M
|
* | FIN_LT_0 |
![]() |
M
| |
* | FIN_GE_0 |
![]() |
M
| |
CARD_INTERV |
![]() |
![]() |
M
| |
b | CARD_EMPTY_INTERV |
![]() |
![]() |
M
|
* | DERIV_LE_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_GE_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_LT_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_GT_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_EQUAL_CARD |
![]() |
![]() ![]() |
M
|
* | FORALL_INST |
![]() |
![]() ![]() |
M
|
* | FORALL_INST_MP |
![]() |
![]() ![]() |
M
|
* | CUT |
![]() |
hypothesis ![]() |
M
|
b | EXISTS_INST |
![]() |
![]() ![]() |
M
|
* | DISTINCT_CASE |
![]() |
case distinction on predicate ![]() |
M
|
ONE_POINT_L |
![]() |
The rule can be applied with ![]() ![]() |
A
| |
ONE_POINT_R |
![]() |
The rule can be applied with ![]() ![]() |
A |