Re: [isabelle] [Isabelle2016-1-RC4] Simplification of numerals very slow when Primes is imported

See now 7705926ee595.

> The evidence may be clear that removing this simprule corrects the
> problem, but there is nothing obviously wrong with the rule. The problem
> may be due to an interaction with some other rule. Is this one really
> the underlying cause?

The reason was the generalization of prime from nat to a generic
algebraic structure, including int.  If you run the example in
Isabelle2016 changing int to nat, you run into the same performance

Again, the overall problem is that simp rules for computing concrete
values are often not apt for abstract reasoning and vice versa.
Nevertheless in this particular case it is surely better to have that
simp rule removed.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.