Difference between revisions of "Extension Proof Rules"

From Event-B
Jump to navigationJump to search
imported>Nicolas
m (Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page.)
imported>WikiSysop
 
(7 intermediate revisions by 3 users not shown)
Line 2: Line 2:
 
Rules without a <tt>*</tt> are planned to be implemented in future versions.
 
Rules without a <tt>*</tt> are planned to be implemented in future versions.
 
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
 
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
 +
 +
=== Rewrite Rules ===
  
 
{{RRHeader}}
 
{{RRHeader}}
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COND_BTRUE}}||<math>  \operatorname{COND}(\btrue, E_1, E_2)  \;\;\defi\;\;  E_1 </math>||  ||  A
+
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BTRUE}}||<math>  \operatorname{COND}(\btrue, E_1, E_2)  \;\;\defi\;\;  E_1 </math>||  ||  A
{{RRRow}}| ||{{Rulename|SIMP_SPECIAL_COND_BFALSE}}||<math>  \operatorname{COND}(\bfalse, E_1, E_2)  \;\;\defi\;\;  E_2 </math>||  ||  A
+
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BFALSE}}||<math>  \operatorname{COND}(\bfalse, E_1, E_2)  \;\;\defi\;\;  E_2 </math>||  ||  A
 +
{{RRRow}}|*||{{Rulename|SIMP_MULTI_COND}}||<math>  \operatorname{COND}(C, E, E)  \;\;\defi\;\;  E </math>||  ||  A
 
|}
 
|}
  
 +
=== Inference Rules ===
 +
{{RRHeader}}
 +
{{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_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})  \;\;\vdash \;\; \textbf{P}(x)  \qquad \ldots \qquad}{ \textbf{H}  \;\;\vdash\;\;  \textbf{P}(x) }</math>|| where <math>x</math> has inductive datatype <math>DT</math> as type and appears free in <math>\textbf{P}</math>; <math>\{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\}</math> are the inductive parameters (if any); an antecedent is created for every constructor <math>c_i</math> of <math>DT</math>; all parameters are introduced as fresh identifiers; examples [[Datatype Rules|here]]  ||  M
 +
|}
  
 
[[Category:User documentation|The Proving Perspective]]
 
[[Category:User documentation|The Proving Perspective]]
 
[[Category:Rodin Platform|The Proving Perspective]]
 
[[Category:Rodin Platform|The Proving Perspective]]
 
[[Category:User manual|The Proving Perspective]]
 
[[Category:User manual|The Proving Perspective]]

Latest revision as of 15:38, 29 November 2019

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)#Rewrite_Rules.

Rewrite Rules

  Name Rule Side Condition A/M
*
SIMP_SPECIAL_COND_BTRUE
  \operatorname{COND}(\btrue, E_1, E_2)  \;\;\defi\;\;  E_1 A
*
SIMP_SPECIAL_COND_BFALSE
  \operatorname{COND}(\bfalse, E_1, E_2)  \;\;\defi\;\;  E_2 A
*
SIMP_MULTI_COND
  \operatorname{COND}(C, E, E)  \;\;\defi\;\;  E A

Inference Rules

  Name Rule Side Condition A/M
*
DATATYPE_DISTINCT_CASE
\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} } where x has a datatype DT as type and appears free in \textbf{G}, DT has constructors c_1, \ldots, c_n, parameters p_{ij} are introduced as fresh identifiers M


*
DATATYPE_INDUCTION
\frac{ \textbf{H}, x=c_1(p_1, \ldots, p_k),\textbf{P}(p_{I_1}), \ldots, \textbf{P}(p_{I_l})  \;\;\vdash \;\; \textbf{P}(x)  \qquad \ldots \qquad}{ \textbf{H}  \;\;\vdash\;\;  \textbf{P}(x) } where x has inductive datatype DT as type and appears free in \textbf{P}; \{p_{I_1}, \ldots, p_{I_l}\} \subseteq \{p_1, \ldots, p_k\} are the inductive parameters (if any); an antecedent is created for every constructor c_i of DT; all parameters are introduced as fresh identifiers; examples here M