Difference between revisions of "Inference Rules"
From Event-B
Jump to navigationJump to searchimported>Nicolas m (added CUT) |
imported>Nicolas m (removed bold font in WD ;; used correct symbol for :=) |
||
Line 139: | Line 139: | ||
{{RRRow}}|*||<font size="-2"> CARD_SUBSETEQ </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \textbf{P}(S \subseteq T) }{\textbf{H} \;\;\vdash\;\; \textbf{P}(\card\,(S) \leq \card(T))}</math> || || M | {{RRRow}}|*||<font size="-2"> CARD_SUBSETEQ </font>|| <math>\frac{\textbf{H} \;\;\vdash \;\; \textbf{P}(S \subseteq T) }{\textbf{H} \;\;\vdash\;\; \textbf{P}(\card\,(S) \leq \card(T))}</math> || || M | ||
− | {{RRRow}}|*||<font size="-2"> FORALL_INST </font>|| <math>\frac{ \;\;\vdash \;\; | + | {{RRRow}}|*||<font size="-2"> FORALL_INST </font>|| <math>\frac{ \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} , [x \bcmeq E]\textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \forall x \qdot \textbf{P} \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> || M |
− | {{RRRow}}|*||<font size="-2"> FORALL_INST_MP </font>|| <math>\frac{ \;\;\vdash \;\; | + | {{RRRow}}|*||<font size="-2"> FORALL_INST_MP </font>|| <math>\frac{ \;\;\vdash \;\; {WD}(E) \qquad \textbf{H}, {WD}(E) \;\;\vdash \;\; [x \bcmeq E]\textbf{P} \qquad \textbf{H}, {WD}(E), [x \bcmeq E]\textbf{Q} \;\;\vdash \;\; \textbf{G}}{\textbf{H}, \forall x \qdot \textbf{P} \limp \textbf{Q} \;\;\vdash\;\; \textbf{G}}</math> || <math>x</math> is instantiated with <math>E</math> and a Modus Ponens is applied|| M |
− | {{RRRow}}|*||<font size="-2"> CUT </font>|| <math>\frac{ \;\;\vdash \;\; | + | {{RRRow}}|*||<font size="-2"> CUT </font>|| <math>\frac{ \;\;\vdash \;\; {WD}(\textbf{P}) \qquad \textbf{H}, {WD}(\textbf{P}) \;\;\vdash \;\; \textbf{\textbf{P}} \qquad \textbf{H}, {WD}(\textbf{P}), \textbf{P} \;\;\vdash \;\; \textbf{G}}{\textbf{H} \;\;\vdash\;\; \textbf{G}}</math> || hypothesis <math>\textbf{P}</math> is added || M |
|} | |} |
Revision as of 14:20, 3 July 2009
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
| |
* | DBL_HYP | ![]() |
A
| |
* | AND_L | ![]() |
A
| |
* | AND_R | ![]() |
A
| |
* | IMP_L1 | ![]() |
A
| |
* | IMP_R | ![]() |
A
| |
* | IMP_AND_L | ![]() |
A
| |
* | IMP_OR_L | ![]() |
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
| |
* | 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_SETMINUS_R | ![]() |
the occurrence of ![]() ![]() ![]() |
M
|
* | SIM_REL_IMAGE_R | ![]() |
the occurrence of ![]() |
M
|
* | SIM_FCOMP_R | ![]() |
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 | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_REL_RAN_R | ![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_REL_DOM_R | ![]() |
the user has to write the set corresponding to ![]() |
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
|
* | CARD_EMPTY_INTERV | ![]() |
![]() |
M
|
* | CARD_SUBSETEQ | ![]() |
M
| |
* | FORALL_INST | ![]() |
![]() ![]() |
M
|
* | FORALL_INST_MP | ![]() |
![]() ![]() |
M
|
* | CUT | ![]() |
hypothesis ![]() |
M |