Inference Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Laurent m FIxed spacing in formulas |
imported>Laurent m Fixed more spacing in formulas |
||
Line 36: | Line 36: | ||
\textbf{H},\textbf{P},\;\textbf{Q}\limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P},\; \textbf{P} \land \textbf{Q} \limp \textbf{R} \;\;\vdash \;\; \textbf{S}}</math> || || A | \textbf{H},\textbf{P},\;\textbf{Q}\limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P},\; \textbf{P} \land \textbf{Q} \limp \textbf{R} \;\;\vdash \;\; \textbf{S}}</math> || || A | ||
{{RRRow}}|*||{{Rulename|NEG_IN_L}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\} \; \; \vdash \; \; | {{RRRow}}|*||{{Rulename|NEG_IN_L}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\} \; \; \vdash \; \; \textbf{P} }{\textbf{H},\; E \in \{ a,\ldots , b, \ldots , c\} , \neg \, (E=b) \; \; \vdash \; \; \textbf{P} }</math> || || A | ||
{{RRRow}}|*||{{Rulename|NEG_IN_R}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\} \; \; \vdash \; \; | {{RRRow}}|*||{{Rulename|NEG_IN_R}}|| <math>\frac{\textbf{H},\; E \in \{ a,\ldots , c\} \; \; \vdash \; \; \textbf{P} }{\textbf{H},\; E \in \{ a,\ldots , b, \ldots , c\} , \neg \, (b=E) \; \; \vdash \; \; \textbf{P} }</math> || || A | ||
{{RRRow}}|*||{{Rulename|XST_L}}|| <math>\frac{\textbf{H},\; \textbf{P(x)} \; \; \vdash \; \; \textbf{Q} | {{RRRow}}|*||{{Rulename|XST_L}}|| <math>\frac{\textbf{H},\; \textbf{P(x)} \; \; \vdash \; \; \textbf{Q} | ||
Line 47: | Line 47: | ||
{{RRRow}}|*||{{Rulename|ALL_R}}|| <math>\frac{\textbf{H}\; \; \vdash \; \; \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \; \forall \textbf{x}\, \qdot\, \textbf{P(x)} }</math> || || A | {{RRRow}}|*||{{Rulename|ALL_R}}|| <math>\frac{\textbf{H}\; \; \vdash \; \; \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \; \forall \textbf{x}\, \qdot\, \textbf{P(x)} }</math> || || A | ||
{{RRRow}}|*||{{Rulename|EQL_LR}}|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \; | {{RRRow}}|*||{{Rulename|EQL_LR}}|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \; \textbf{P(E)} }{\textbf{H(x)},\; x=E \; \; \vdash \; \; \textbf{P(x)} }</math> || <math>x</math> is a variable which is not free in <math>E</math> || A | ||
{{RRRow}}|*||{{Rulename|EQL_RL}}|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \; | {{RRRow}}|*||{{Rulename|EQL_RL}}|| <math>\frac{\textbf{H(E)} \; \; \vdash \; \; \textbf{P(E)} }{\textbf{H(x)},\; E=x \; \; \vdash \; \; \textbf{P(x)} }</math> || <math>x</math> is a variable which is not free in <math>E</math> || A | ||
{{RRRow}}| ||{{Rulename|SUBSET_INTER}}|| <math>\frac{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\; | {{RRRow}}| ||{{Rulename|SUBSET_INTER}}|| <math>\frac{\textbf{H},\;\textbf{T} \subseteq \textbf{U} \;\;\vdash \;\; |
Revision as of 17:46, 11 November 2009
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 and denote types 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 |
the operator must appear at the "top level" | A
| ||
IN_INTER |
the operator must appear at the "top level" | A
| ||
NOTIN_INTER |
the operator must appear at the "top level" | 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
| ||
b | MH |
M
| ||
b | HM |
M
| ||
* | EQV |
M
| ||
* | OV_L |
the operator must appear at the "top level" | M
| |
* | OV_R |
the operator must appear at the "top level" | M
| |
* | OV_L |
the operator must appear at the "top level" | M
| |
* | OV_R |
the operator must appear at the "top level" | M
| |
* | DIS_BINTER_R |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | DIS_BINTER_L |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | DIS_SETMINUS_R |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | DIS_SETMINUS_L |
the occurrence of must appear at the "top level". Moreover and denote some type. | M
| |
* | SIM_REL_IMAGE_R |
the occurrence of must appear at the "top level". | M
| |
* | SIM_REL_IMAGE_L |
the occurrence of must appear at the "top level". | M
| |
* | SIM_FCOMP_R |
the occurrence of must appear at the "top level". | M
| |
* | SIM_FCOMP_L |
the occurrence of must appear at the "top level". | M
| |
b | 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_SETMINUS_R |
M
| ||
b | 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 |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_REL_RAN_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_REL_DOM_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN1_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN2_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN_IMG_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | FIN_FUN_RAN_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
b | 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 |
must appear at "top-level" | M
| |
b | CARD_EMPTY_INTERV |
must appear at "top-level" | M
| |
b | CARD_SUBSETEQ |
and bear the same type | M
| |
* | FORALL_INST |
is instantiated with | M
| |
* | FORALL_INST_MP |
is instantiated with and a Modus Ponens 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 |