[isabelle-dev] HOL/Number_Theory/Primes

[Dmitriy Traytel]

The culprit seems to be dvd_imp_mod_0 introduced as a simp rule in 
773b378d9313.

The following takes again only 2 seconds.

declare dvd_imp_mod_0[simp del]
lemma "prime(97::nat)" by simp

Dmitriy

On 07.11.2014 15:31, Tobias Nipkow wrote:
> Very nice observations, thank you. I was obviously too hasty to remove 
> the test which exposed this time leak. Once this issue has been fixed, 
> I will put the "long" test back in, with a better comment.
>
> Tobias
>
> On 07/11/2014 15:27, Dmitriy Traytel wrote:
>> 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 
>>>
>>
>> _______________________________________________
>> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141107/36d3e45e/attachment-0002.html>