Splitting 'and' conditions into multiple conditions
Quote:
> The simplifier is often unable to prove easy conclusions, because conditions
> given als assert, precondition, and postcondition occur as a single
> conclusion.
> Example:
> C1: res__1 >= buf__first and res__1 <= buf__last and (res__1 >= 0 and res__1
> <= 0) -> res__1 >= buf__first and res__1 <= buf__last .
> Or do I misinterpret this line containing an implication?
> Should the simplifier not able to handle this by transfering the frist part
> to the hypothis?
Lutz,
We are always interested in collecting examples where the Simplifier can
be improved. You should note, however, that the Simplifier is just
that, it is not intended to be a heavyweight proof engine like PVS. The
idea is to limit what the Simplifier gets up to so as to maintain clear
traceability between what goes into it and what comes out and to avoid
the possibility of multiple substitutions leaving the formulae in a
worse state than they started. The unsimplified VCs that are left can
always be tacked with the interactive Prof Checker tool.
Peter