[isabelle-dev] HOL/Number_Theory/Primes

[Dmitriy Traytel]

This is in Isabelle2014. In 229765cc3414 I make the same measurements as 
Larry. So indeed (as the text above those lemmas suggests) there seems 
to be a regression with the simplifier setup.

Dmitriy

On 07.11.2014 15:10, Julian Brunner wrote:
> The proof that 97 is prime only takes 1.3s on my machine (2.7 GHz i7),
> with the whole theory Primes loading in about 4 seconds.
>
> On Wed, Nov 5, 2014 at 8:37 PM, Florian Haftmann
> <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>> This theory takes quite a while to load, and I have found out why:
>>>
>>> text{* A bit of regression testing: *}
>>>
>>> lemma "prime(97::nat)" by simp
>>> lemma "prime(997::nat)" by eval
>>>
>>> The proof that 97 is prime takes 35 seconds on a very fast machine. Can we get rid of this or at least substitute a smaller number?
>> The question is whether this has really to be performed using simp.
>>
>> As an alternative, a suitable code equations could be proven using the
>> primes_upto in Eratosthenes.thy, but I did never take any measurements
>> at which threshold the additional data structures outperform brute-force
>> calculation.
>>
>>          Florian
>>
>> --
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev