I would agree that changing simp rules to avoid using "neg" is not a huge improvement in and of itself. At best, it can reduce the number of rewrite steps needed to solve some arithmetic subgoals.
However, speeding up simplification was not my primary goal. I share the opinion of Makarius that we would be much better off with numerals based on the natural numbers, rather than the integers. This would let us have a nice, clean way of doing arithmetic on arbitrary semirings - the ad-hoc, ugly, and inefficient rewrite rules in NatBin would no longer be needed. I think that the transition to nat-based numerals will be facilitated by cleaning up the simplification rules for arithmetic, and removing any unnecessary uses of subtraction (e.g. less_number_of_eq_neg and friends). - Brian Quoting Lawrence Paulson <lp15 at cam.ac.uk>: > When I introduced these constants, they were certainly necessary. Then, > binary arithmetic executed by pure rewriting. I don't object to getting > rid of them if they are now unnecessary. But it hardly seems worth > investing a significant effort. They don't cause a problem, do they? It > may be best to leave well enough alone. > Larry