Re: [isabelle] Non-idempotence of datatype constructors



I cleaned up and optimised my simproc a little bit more [1] and ran some
tests [2]. In particular, I realised that it makes no sense for it to
work on lists since other simprocs already handle the problem there.

Both tests on my machine and on the Testboard seem to indicate that, on
average, the simproc leads to about 0.7% to 1.0% slowdown (both elapsed
time and CPU time).

Tobias and I think the simproc is interesting enough to switch on by
default (it makes trivial and obvious proof obligations go away).

Dmitriy and Jasmin were concerned that it might not be worth the
slowdown and that it should be discussed on the list. Jasmin thinks it
might not be useful often enough to justify a 1% slowdown and should
therefore not be enabled by default.

I on the other hand think that any simproc that is not enabled by
default will simply never be used in practice so that if we don't enable
it by default, we might as well not have it in the first place.

Feel free to weigh in on this, everyone!

Manuel

[1]: http://isabelle.in.tum.de/repos/testboard/rev/f13520ad9b93
[2]: https://ci.isabelle.systems/jenkins/job/testboard/320/




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