Re: [isabelle] Cancellation simprocs



Hi Mathias,

> To solve the problem, I have locally activated GeMS where I have
> hard-coded that the simproc does not apply on types where LPS applies.
> It worked without problem. However, I am not sure that testing the AFP
> and the Isabelle distribution is sufficient to declare that (3) does not
> cause problems.

> Does somebody have an opinion on the matter? Or should I just proceed
> and activate my GeMS simproc on all cancel_comm_monoid_add types (except
> those where LPS applies)?

operationally this should be OK.  But the overall design seems not very
convincing.

I have no ready-to-proceed suggestion at hand, but a few thoughts:

* LPS is the only one to operate on nat / int directly rather than an
algebraic structure.  Can this be lifted, and how would the overall
picture then look like?
* Can there be *one* implementation of GeMS and LPS with a case
distinction or something like that?  That would still be better two
concurring implementations.
* Note that technically the cancellation simproc implementations are
notoriously outdated;  the state of the are is to implement such a
simproc in a locale and then interpret it onto the desired instances.
Detail can be found in Amine Chaieb and Makarius Wenzel: Context aware
Calculation and Deduction --- Ring Equalities via GrÃbner Bases in
Isabelle.  And in src/HOL/Semiring_Normalization.thy

Best,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.