[isabelle-dev] Bug in linordered_ring_less_cancel_factor simproc

[Florian Haftmann]

Hi Brian,

> Here is the changeset that introduced the "aconv" test:
> http://isabelle.in.tum.de/repos/isabelle/rev/7cdcc9dd95cb
>
> I'm not sure why the "aconv" test is there, so I don't want to remove
> it myself. Could someone else please look into this?

The aconv has already been present previously:
http://isabelle.in.tum.de/repos/isabelle/rev/7cdcc9dd95cb#l8.15

The numeral simprocs (like more arithemtic matter) are, more or less, a
mess.  We don't even know how relevant they are nowadays.  So, if no
complaint arises to remove the aconv test and no problems occur, it
could be the best option to drop it.

> After some investigation, I have concluded that the problem has to do
> with Arith_Data.prove_conv.
> Arith_Data.prove_conv is
> called to move the common term to the left, so it matches the rules
> mult_less_cancel_left_pos or mult_less_cancel_left_neg.

This is a worthwhile observation -- if you like you could document this
in a rename of prove_conv to, say, prove_common_leftmost.

> Also, we really need to have some proper regression tests for
> simprocs. Currently the only tests for these simprocs are in a
> commented-out (!) section of Tools/numeral_simprocs.ML.

Sound like a potential candidate for a HOL/ex theory.

> First of all, the ML antiquotation @{simproc
> linordered_ring_less_cancel_factor simproc} doesn't work. Why? The
> simproc is listed by name when I ask ProofGeneral to print out the
> simpset. With no way to refer to the existing simproc from ML, I had
> to cut-and-paste a copy of all the simproc ML code in order to test it
> individually.

This antiquotation only works for new-style named simprocs, which the
numeral simprocs are definitely not.

This is a good place for some general observations concerning this matter.

a) The state-of-the art for implementing domain-specific proof
procedures in Isabelle is described in Context aware Calculation and
Deduction by Chaieb and Wenzel,
http://www4.in.tum.de/~chaieb/pubs/pdf/morphism.pdf.  Unfortunately,
AFAIK this has not spread wider than the Groebner bases stuff (indeed
the currently emering Semiring_Normalizer theory is a good example, I
think).

b) The current numeral representation is a matter on its own (I supppose
you know very well).

c) The whole look-and-feel of these simprocs is very odd nowadays
(functor instantiation, global magic etc.)

d) It is not clear how far those simprocs are (or could) subsumed by
more advanced proof procedures.

Doing it right would mean to investigate d) first, understanding a),
implementing the necessary simporcs using a), thus solving c), and
perhaps pave the way for tackling b) in the end.  So far no body was
adventurous enough to start this ;-)


Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100510/6df471ab/attachment.sig>