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
