Inference Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas added DATATYPE_DISTINCT_CASE |
imported>Nicolas added DATATYPE_INDUCTION; rewrote DATATYPE_DISTINCT_CASE |
||
Line 193: | Line 193: | ||
{{RRRow}}| ||{{Rulename|ONE_POINT_R}}||<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>|| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> || A | {{RRRow}}| ||{{Rulename|ONE_POINT_R}}||<math>\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }</math>|| The rule can be applied with <math>\forall</math> as well as with <math>\exists</math> || A | ||
{{RRRow}}| ||{{Rulename|DATATYPE_DISTINCT_CASE}}||<math>\frac{\textbf{H}, x= | {{RRRow}}| ||{{Rulename|DATATYPE_DISTINCT_CASE}}||<math>\frac{\textbf{H}, x=c_1(p_{11}, \ldots, p_{1k}) \;\;\vdash \;\; \textbf{G} \qquad \ldots \qquad \textbf{H}, x=c_n(p_{n1}, \ldots, p_{nl}) \;\;\vdash \;\; \textbf{G} }{ \textbf{H} \;\;\vdash\;\; \textbf{G} }</math>|| where <math>x</math> has a datatype <math>DT</math> as type and appears free in <math>\textbf{G}</math>, <math>DT</math> has constructors <math>c_1, \ldots, c_n</math>, parameters <math>p_{ij}</math> are introduced as fresh identifiers || M | ||
{{RRRow}}| ||{{Rulename|DATATYPE_INDUCTION}}||<math>\frac{\textbf{H}, x=c_N(\ldots) \;\;\vdash \;\; \textbf{P}(c_N(\ldots)) \qquad \textbf{H}, x=c_I(p_N, p_I),\textbf{P}(p_I) \;\;\vdash \;\; \textbf{P}(c_I(p_N, p_I)) }{ \textbf{H} \;\;\vdash\;\; \textbf{P}(x) }</math>|| (N = Non inductive; I = Inductive) where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>c</math> are constructors of <math>DT</math>; an antecedent is created for each <math>c_N</math> and each <math>c_I</math>, an hypothesis <math>\textbf{P}(p_I)</math> is added for each <math>p_I</math>; all parameters are introduced as fresh identifiers || M | |||
|} | |} |
Revision as of 13:55, 6 August 2010
CAUTION! Any modification to this page shall be announced on the User mailing list!
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
| ||
* | 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
| ||
* | MH |
M
| ||
* | HM |
M
| ||
EQV |
M
| |||
* | OV_SETENUM_L |
the operator must appear at the "top level" | A
| |
* | OV_SETENUM_R |
the operator must appear at the "top level" | A
| |
* | OV_L |
the operator must appear at the "top level" | A
| |
* | OV_R |
the operator must appear at the "top level" | A
| |
* | 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
| |
* | 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 |
M
| ||
* | FIN_REL_RAN_R |
M
| ||
* | FIN_REL_DOM_R |
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
| ||
* | 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 |
must appear at "top-level" | M | ||
SIMP_CARD_SETMINUS_R |
must appear at "top-level" | M
| ||
SIMP_CARD_CPROD_L |
must appear at "top-level" | M | ||
SIMP_CARD_CPROD_R |
must appear at "top-level" | 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
| ||
DATATYPE_DISTINCT_CASE |
where has a datatype as type and appears free in , has constructors , parameters are introduced as fresh identifiers | M
| ||
DATATYPE_INDUCTION |
(N = Non inductive; I = Inductive) where has inductive datatype as type and appears free in ; are constructors of ; an antecedent is created for each and each , an hypothesis is added for each ; all parameters are introduced as fresh identifiers | M |