[isabelle-dev] HOL/Number_Theory/Primes
Lawrence Paulson
lp15 at cam.ac.uk
Fri Nov 7 20:09:06 CET 2014
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 <nipkow at 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].
More information about the isabelle-dev
mailing list