Inference Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Laurent m Renamed SIM_FUN into FUN_GOAL. |
imported>Laurent mNo edit summary |
||
Line 13: | Line 13: | ||
{{RRRow}}|*||<font size="-2"> TRUE_GOAL </font>|| <math>\frac{}{\textbf{H} \;\;\vdash \;\; \btrue}</math> || || A | {{RRRow}}|*||<font size="-2"> TRUE_GOAL </font>|| <math>\frac{}{\textbf{H} \;\;\vdash \;\; \btrue}</math> || || A | ||
{{RRRow}}|*||<font size="-2"> FUN_GOAL </font>|| <math>\frac{}{\textbf{H},\; f\in | {{RRRow}}|*||<font size="-2"> FUN_GOAL </font>|| <math>\frac{}{\textbf{H},\; f\in \textbf{E}\;\mathit{op}\; \textbf{F} \;\;\vdash\;\; f\in T_1\pfun T_2}</math> || where <math>T_1</math> and <math>T_2</math> denote types and <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}}|*||<font size="-2"> DBL_HYP </font>|| <math>\frac{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H},\;\textbf{P},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> || || A | {{RRRow}}|*||<font size="-2"> DBL_HYP </font>|| <math>\frac{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}{\textbf{H},\;\textbf{P},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math> || || A |
Revision as of 13:28, 6 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
| ||
* | 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
| ||
* | 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
| ||
* | CONTRADICT_L | M
| ||
* | CONTRADICT_R | M
| ||
* | CASE | M
| ||
* | MH | M
| ||
* | 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. Similar left distribution rules exist | M
| |
* | DIS_SETMINUS_R | the occurrence of must appear at the "top level". Moreover and denote some type. Similar left distribution rules exist | M
| |
* | SIM_REL_IMAGE_R | the occurrence of must appear at the "top level". A similar left simplification rule exists. | M
| |
* | SIM_FCOMP_R | the occurrence of must appear at the "top level". A similar left simplification rule exists. | 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_SETMINUS_R | M
| ||
* | 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
| |
* | 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 | must appear at "top-level" | M
| |
* | CARD_EMPTY_INTERV | must appear at "top-level" | M
| |
* | CARD_SUBSETEQ | 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 |