[isabelle-dev] Bug in linordered_ring_less_cancel_factor simproc

[Makarius]

On Mon, 10 May 2010, Florian Haftmann wrote:

>> 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

I think it all goes back to this version:
http://isabelle.in.tum.de/repos/isabelle/rev/22d4c641ebff#l1.154
or maybe even earlier.

IIRC the numeral simprocs belong to the second wave of, after I've 
introduced the mechanism and produced the more basic ones around functor 
CancelFactorFun.  Looking there, e.g. 
http://isabelle.in.tum.de/repos/isabelle/annotate/92cc2f4c7335/src/Provers/Arith/cancel_factor.ML#l71 
you see that the internal "conversion" prover does not have this optional 
result, although at the outermost level simprocs usually try to fail 
quickly on problems that are out of their scope, e.g. being too trivial or 
too hard.

This might be the source of the reflexivity test by Larry, although it 
might have moved in further than expected.  Maybe Larry recalls what he 
did 10 years ago in 22d4c641ebff.


> 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.

> 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 ;-)

Yes, this has been the situation for many years already.  Such ancient 
things will cause many surprises when changed too quickly, i.e. it is 
something to do after the release.


 	Makarius