[isabelle-dev] HOL/Number_Theory/Primes

[Julian Brunner]

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
>