Improved WD Lemma Generation

From Event-B
Revision as of 09:45, 21 April 2010 by imported>Laurent (Added first motivating example)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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 f(x) = f(y) is

f\in S\pfun T\land x\in\dom(f)\land f\in S\pfun T\land y\in\dom(f)

This predicate is sub-optimal as it contains twice the same sub-predicate (f\in S\pfun T). Consequently, when the prover is fed with the generated lemma, it will have to prove twice the same goal.