Difference between revisions of "Inference Rules"
From EventB
Jump to navigationJump to searchimported>Nicolas m (Added INDUC_* inference rules) 
imported>Nicolas m (Removed induction on integers (was wrong), reviewed induciton on naturals) 

Line 229:  Line 229:  
{{RRRow}}*{{RulenameSIM_OV_TFUN}} <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math>  where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math>  A  {{RRRow}}*{{RulenameSIM_OV_TFUN}} <math> \frac{\textbf{H}\vdash x\in A\qquad \textbf{H}\vdash y\in B}{\textbf{H}, f\in A\;op\; B\vdash f\ovl\left\{x\mapsto y\right\}\in A\tfun B} </math>  where <math>\mathit{op}</math> is one of <math>\tfun</math>, <math>\tinj</math>, <math>\tsur</math>, <math>\tbij</math>  A  
−  {{RRRow}} {{RulenameINDUC_NAT}} <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(  +  {{RRRow}} {{RulenameINDUC_NAT}} <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H}, x=0 \;\;\vdash \;\; \textbf{P}(x) \qquad \textbf{H}, n\in\nat, \textbf{P}(n) \;\;\vdash \;\; \textbf{P}(n+1)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math>  <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math>; <math>n</math> is introduced as a fresh identifier  M 
−  {{RRRow}} {{RulenameINDUC_NAT_COMPL}} <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, k\  +  {{RRRow}} {{RulenameINDUC_NAT_COMPL}} <math>\frac{\textbf{H} \;\;\vdash \;\; x\in\nat \qquad \textbf{H} \;\;\vdash \;\; \textbf{P}(0) \qquad \textbf{H}, n\in\nat, \forall k\qdot 0\leq k\land k < n \limp \textbf{P}(k) \;\;\vdash \;\; \textbf{P}(n)}{\textbf{H} \;\;\vdash\;\; \textbf{P}(x)}</math>  <math>x</math> of type <math>\intg</math> appears free in <math>\textbf{P}</math>; <math>n</math> is introduced as a fresh identifier  M 
−  
−  
−  
−  
Latest revision as of 16:00, 23 June 2014
CAUTION! Any modification to this page shall be announced on the User mailing list!
Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Inference_Rules.
Name  Rule  Side Condition  A/M
 

*  HYP 
see below for  A
 
*  HYP_OR 
see below for  A
 
*  CNTR 
see below for  A
 
*  FALSE_HYP 
A
 
*  TRUE_GOAL 
A
 
*  FUN_GOAL 
where and denote types and is one of , , , , , , .  A
 
*  FUN_IMAGE_GOAL 
where denotes a set of relations (any arrow) and is WD strict  M
 
FUN_GOAL_REC 
where and denote types, denotes a set of relations (any arrow) 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 
where and are not bound by  A
 
IN_INTER 
where and are not bound by  A
 
NOTIN_INTER 
where and are not bound by  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
 
*  IMP_CASE 
M
 
*  MH 
M
 
*  HM 
M
 
EQV_LR 
M
 
EQV_RL 
M
 
*  OV_SETENUM_L 
where is WD strict  A
 
*  OV_SETENUM_R 
where is WD strict  A
 
*  OV_L 
where is WD strict  A
 
*  OV_R 
where is WD strict  A
 
*  DIS_BINTER_R 
where and denote types.  M
 
*  DIS_BINTER_L 
where and denote types.  M
 
*  DIS_SETMINUS_R 
where and denote types.  M
 
*  DIS_SETMINUS_L 
where and denote types.  M
 
*  SIM_REL_IMAGE_R 
M
 
*  SIM_REL_IMAGE_L 
M
 
*  SIM_FCOMP_R 
M
 
*  SIM_FCOMP_L 
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_KINTER_R 
where is fresh  M
 
FIN_QINTER_R 
M
 
*  FIN_SETMINUS_R 
M
 
FIN_REL 
where denotes a set of relations (any arrow)  A
 
*  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_FUN_DOM 
where is one of , , , , , ,  A
 
FIN_FUN_RAN 
where is one of , ,  A
 
*  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 
where is WD strict  M
 
CARD_EMPTY_INTERV 
where is WD strict  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 
M  
SIMP_CARD_SETMINUS_R 
M
 
SIMP_CARD_CPROD_L 
M  
SIMP_CARD_CPROD_R 
M
 
*  FORALL_INST 
is instantiated with  M
 
*  FORALL_INST_MP 
is instantiated with and a Modus Ponens is applied  M
 
*  FORALL_INST_MT 
is instantiated with and a Modus Tollens 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
 
*  SIM_OV_REL 
where is one of , , , , , , , , , ,  A
 
*  SIM_OV_TREL 
where is one of , , ,, ,  A
 
*  SIM_OV_PFUN 
where is one of , , , , , ,  A
 
*  SIM_OV_TFUN 
where is one of , , ,  A
 
INDUC_NAT 
of type appears free in ; is introduced as a fresh identifier  M
 
INDUC_NAT_COMPL 
of type appears free in ; is introduced as a fresh identifier  M

Those following rules have been implemented in the reasoner GeneralizedModusPonens.
Name  Rule  Side Condition  A/M  

*  GENMP_HYP_HYP 
see below for  A  
*  GENMP_NOT_HYP_HYP 
see below for  A  
*  GENMP_HYP_GOAL 
see below for  A  
*  GENMP_NOT_HYP_GOAL 
see below for  A  
*  GENMP_GOAL_HYP 
see below for  A  
*  GENMP_NOT_GOAL_HYP 
see below for  A  
*  GENMP_OR_GOAL_HYP 
see below for  A  
*  GENMP_OR_NOT_GOAL_HYP 
see below for  A 
Thos following rules have been implemented in the MembershipGoal reasoner.
Name  Rule  Side Condition  A/M
 

*  SUBSET_SUBSETEQ 
A  
*  DOM_SUBSET 
A  
*  RAN_SUBSET 
A  
*  EQUAL_SUBSETEQ_LR 
A  
*  EQUAL_SUBSETEQ_RL 
A  
*  IN_DOM_CPROD 
A  
*  IN_RAN_CPROD 
A  
*  IN_DOM_REL 
A  
*  IN_RAN_REL 
A  
*  SETENUM_SUBSET 
A  
*  OVR_RIGHT_SUBSET 
A  
*  RELSET_SUBSET_CPROD 
where is one of , , , , , , , , , ,  A  
*  DERIV_IN_SUBSET 
A 
The conventions used in this table are described in Variations in HYP, CNTR and GenMP.
Side Condition  



where a and b are integers  








where A and B are sets  






where e and f are scalars  
See also Extension Proof Rules#Inference Rules.