[isabelle-dev] Numeral simplification: neg and iszero

[Brian Huffman]

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