Hi Artur,

In your example the residual existential quantification arising from the predicate of Op can be entirely eliminated using the one-point rule for exists. I've implemented some SML functions some time ago that realise such simplifications for existential quantifiers as a ProofPower rule as well as conversion (!), for Z as well as HOL quantifiers.

Attached is the source code of the relevant functions. The conversion z_exists_one_point_conv, for instance, works entirely automatic, consecutively eliminating all existential quantified variables for which there exists some conjunct v = E in the body of the quantification. It might help you to automatically simplify some existential quantifiers. In particular, try and apply the tactic

  (conv_tac (ONCE_MAP_C z_exists_one_point_conv))

to the last goal for Op in your example. It will not entirely eliminate the existential quantifier in the conclusion because symmetric equalities E = v are not exploited yet to eliminate v; you may want to have a look and tweak the source code to incorporate this feature. It may then be possible to entirely eliminate the inner existential quantifier in your example. Otherwise, I shall revise the code at some point to support this feature.

The implementation is still prototypical, and I know some cases in which it will definitely fail, i.e. if there is some recursive dependency in the equalities used to eliminate the variable. (At the moment this will cause an infinite loop rather than an error as would be better).

Hope this may be useful, let me know if you have any problems,


 Dr Dipl.-Inform. Frank Zeyda
 Research Associate
 High Integrity Systems Engineering Group
 Department of Computer Science
 University of York (UK)
 Email: ze...@cs.york.ac.uk
 Phone: 0044-(0)1904-433244
 WWW: http://www-users.cs.york.ac.uk/~zeyda/

Artur Oliveira Gomes wrote:
> Hi there,
> I am having few problems with the precondition calculus. More specifcly,
> I can not say if an existential quantifier included in the predicate of the operation > can be eliminated during the calculus, or if it is the precondition itself.
> Here follows an attached file with a small example of what I am trying to do.
> Best regards,
> --
> Artur Oliveira Gomes
> ------------------------------------------------------------------------
> _______________________________________________
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Attachment: z_exists_one_point_conv.doc
Description: MS-Word document

Proofpower mailing list

Reply via email to