Difference between revisions of "Extension Proof Rules"
From Event-B
Jump to navigationJump to searchimported>Nicolas m (Extension Rewrite Rules moved to Extension Proof Rules: Gathering rewrite and inference rules for extensions in the same page.) |
imported>Nicolas m |
||
| 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 |
|} | |} | ||
| + | |||
| + | == Inference Rules == | ||
| + | {{RRHeader}} | ||
| + | |||
| + | |} | ||
[[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]] | ||
Revision as of 10:27, 9 September 2010
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 |
 |
A | |
| * | SIMP_SPECIAL_COND_BFALSE |
 |
A |
Inference Rules
| Name | Rule | Side Condition | A/M |
|---|
