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
