Difference between revisions of "Improved WD Lemma Generation"
From Event-B
Jump to navigationJump to searchimported>Laurent (Added first motivating example) |
imported>Desaperh |
||
Line 7: | Line 7: | ||
This predicate is sub-optimal as it contains twice the same sub-predicate (<math>f\in S\pfun T</math>). Consequently, when the prover is fed with the generated lemma, it will have to prove twice the same goal. | This predicate is sub-optimal as it contains twice the same sub-predicate (<math>f\in S\pfun T</math>). Consequently, when the prover is fed with the generated lemma, it will have to prove twice the same goal. | ||
+ | |||
+ | The well-definedness lemma generated for predicate <math> x \div y=5 </math> | ||
[[Category:Developer documentation]] | [[Category:Developer documentation]] |
Revision as of 10:53, 21 April 2010
This page describes work in progress for optimising well-definedness lemmas generated by the Core Rodin platform.
Motivating examples
With Rodin 1.3, the well-definedness lemma generated for predicate is
This predicate is sub-optimal as it contains twice the same sub-predicate (). Consequently, when the prover is fed with the generated lemma, it will have to prove twice the same goal.
The well-definedness lemma generated for predicate