[isabelle-dev] HOL/Number_Theory/Primes

[Lawrence Paulson]

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].