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

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.