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.haftm...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
