[isabelle-dev] HOL/Number_Theory/Primes

[Florian Haftmann]

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>