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
bottleneck.

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.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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