Re: [isabelle-dev] HOL/Number_Theory/Primes
So it would be an option to spell out simplification rules for »numeral ?x dvd numeral ?y« explicitly using type class semiring_numeral_div. That sounds like a good solution. It reduces the interdependcies. See now http://isabelle.in.tum.de/reports/Isabelle/rev/18750e86d5b8 and http://isabelle.in.tum.de/reports/Isabelle/rev/2e19b392d9e3 Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
Indeed, the rule does make sense. Can you quantify how much it helped when you added it? Difficult to say. Historically, developments concerning dvd and div are not very connected so far, but I hope this will change gradually as more number theory concepts come in. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
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
Re: [isabelle-dev] HOL/Number_Theory/Primes
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
Re: [isabelle-dev] HOL/Number_Theory/Primes
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.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
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
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.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
___
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
Re: [isabelle-dev] HOL/Number_Theory/Primes
Thanks for finding this out. The theorem is
a dvd b == b mod a = 0
This applies to any term a mod b and creates a subgoal a dvd b. Normally,
that is not too bad. But if a and b are numerals, this leads to a loop with the
rewrite rule Divides.dvd_eq_mod_eq_0_numeral:
(numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0)
The enormous runtimes where due to this loop. It was not an infinite loop
because the simplifier has a depth limit.
Clearly, we cannot have such a loop. Either mod can use dvd or the other way
around, but not both.
Thanks for simp_trace_new/Lars Hupel, it made it easy to find out what was going
on. [It would be nice if the trace could also show when the depth limit is
exceeded, it does not seem to].
Tobias
On 07/11/2014 17:45, Dmitriy Traytel wrote:
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.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
___
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
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
Is this another application for the new NOMATCH simproc?
--
Peter
On Fr, 2014-11-07 at 18:34 +0100, Tobias Nipkow wrote:
Thanks for finding this out. The theorem is
a dvd b == b mod a = 0
This applies to any term a mod b and creates a subgoal a dvd b. Normally,
that is not too bad. But if a and b are numerals, this leads to a loop with
the
rewrite rule Divides.dvd_eq_mod_eq_0_numeral:
(numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0)
The enormous runtimes where due to this loop. It was not an infinite loop
because the simplifier has a depth limit.
Clearly, we cannot have such a loop. Either mod can use dvd or the other way
around, but not both.
Thanks for simp_trace_new/Lars Hupel, it made it easy to find out what was
going
on. [It would be nice if the trace could also show when the depth limit is
exceeded, it does not seem to].
Tobias
On 07/11/2014 17:45, Dmitriy Traytel wrote:
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.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
___
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
On 07/11/2014 19:05, Peter Lammich wrote:
Is this another application for the new NOMATCH simproc?
One could patch this particular problem, but I would be very uneasy with a setup
that has no clear rewrite ordering between these two functions.
Tobias
--
Peter
On Fr, 2014-11-07 at 18:34 +0100, Tobias Nipkow wrote:
Thanks for finding this out. The theorem is
a dvd b == b mod a = 0
This applies to any term a mod b and creates a subgoal a dvd b. Normally,
that is not too bad. But if a and b are numerals, this leads to a loop with the
rewrite rule Divides.dvd_eq_mod_eq_0_numeral:
(numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0)
The enormous runtimes where due to this loop. It was not an infinite loop
because the simplifier has a depth limit.
Clearly, we cannot have such a loop. Either mod can use dvd or the other way
around, but not both.
Thanks for simp_trace_new/Lars Hupel, it made it easy to find out what was going
on. [It would be nice if the trace could also show when the depth limit is
exceeded, it does not seem to].
Tobias
On 07/11/2014 17:45, Dmitriy Traytel wrote:
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.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
___
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
Surely a dvd b == b mod a = 0” should not be a simple. It can’t be such a difficult change. Larry On 7 Nov 2014, at 17:34, Tobias Nipkow nip...@in.tum.de wrote: Thanks for finding this out. The theorem is a dvd b == b mod a = 0 This applies to any term a mod b and creates a subgoal a dvd b. Normally, that is not too bad. But if a and b are numerals, this leads to a loop with the rewrite rule Divides.dvd_eq_mod_eq_0_numeral: (numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0) The enormous runtimes where due to this loop. It was not an infinite loop because the simplifier has a depth limit. Clearly, we cannot have such a loop. Either mod can use dvd or the other way around, but not both. Thanks for simp_trace_new/Lars Hupel, it made it easy to find out what was going on. [It would be nice if the trace could also show when the depth limit is exceeded, it does not seem to]. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
Hi all, On 07.11.2014 18:34, Tobias Nipkow wrote: Thanks for finding this out. The theorem is (A) a dvd b == b mod a = 0 This applies to any term a mod b and creates a subgoal a dvd b. Normally, that is not too bad. But if a and b are numerals, this leads to a loop with the rewrite rule Divides.dvd_eq_mod_eq_0_numeral: (B) (numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0) The enormous runtimes where due to this loop. It was not an infinite loop because the simplifier has a depth limit. Clearly, we cannot have such a loop. Either mod can use dvd or the other way around, but not both. a simple solution would to take out (A) as simp rule again. On the other hand, the rule makes perfectly sense (similar to something like n m == n - m = 0). So it would be an option to spell out simplification rules for »numeral ?x dvd numeral ?y« explicitly using type class semiring_numeral_div. I would take care of this if nobody objects. Thanks for figuring out, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
On 08/11/2014 08:42, Florian Haftmann wrote: Hi all, On 07.11.2014 18:34, Tobias Nipkow wrote: Thanks for finding this out. The theorem is (A) a dvd b == b mod a = 0 This applies to any term a mod b and creates a subgoal a dvd b. Normally, that is not too bad. But if a and b are numerals, this leads to a loop with the rewrite rule Divides.dvd_eq_mod_eq_0_numeral: (B) (numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0) The enormous runtimes where due to this loop. It was not an infinite loop because the simplifier has a depth limit. Clearly, we cannot have such a loop. Either mod can use dvd or the other way around, but not both. a simple solution would to take out (A) as simp rule again. On the other hand, the rule makes perfectly sense (similar to something like n m == n - m = 0). Indeed, the rule does make sense. Can you quantify how much it helped when you added it? So it would be an option to spell out simplification rules for »numeral ?x dvd numeral ?y« explicitly using type class semiring_numeral_div. That sounds like a good solution. It reduces the interdependcies. Tobias I would take care of this if nobody objects. Thanks for figuring out, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL/Number_Theory/Primes
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?
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
Sure, I'll do that.
Tobias
On 05/11/2014 18:36, Lawrence Paulson 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?
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Number_Theory/Primes
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
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
