florian.haftmann at informatik.tu-muenchen.de
Sat Nov 8 08:42:42 CET 2014
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
Thanks for figuring out,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev