[isabelle-dev] HOL/Number_Theory/Primes

[Tobias Nipkow]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141108/7f63d346/attachment.bin>