[isabelle-dev] Numeral simplification: neg and iszero
brianh at cs.pdx.edu
Tue Dec 9 18:42:19 CET 2008
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).
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.
More information about the isabelle-dev