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
