[isabelle-dev] HOL/Number_Theory/Primes
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Sat Nov 8 08:42:42 CET 2014
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141108/1fa9e473/attachment.sig>
More information about the isabelle-dev
mailing list