Quoting Tobias Nipkow nipkow at in.tum.de:
They have been on my get-rid-of list for some time, but when I initially
tried, I noticed they were needed for doing arithmetic. Now that
somebody (Florian?) added less_int_code, it may indeed be a simple job.
Go for it!
Tobias
I figured I should
NatBin.thy is now nearly neg-free, but there are still some other
places with lemmas that use neg. For example, Tools/
ComputeNumeral.thy seems to be a complete re-implementation of the
simpset defined in NatBin.thy for arithmetic at type nat. If such
other lemmas involving neg can be
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
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
They have been on my get-rid-of list for some time, but when I initially
tried, I noticed they were needed for doing arithmetic. Now that
somebody (Florian?) added less_int_code, it may indeed be a simple job.
Go for it!
Tobias
Brian Huffman schrieb:
Is there any good reason why the constants
Hi Brian,
Is there any good reason why the constants neg and iszero (defined
in Int.thy) are needed anymore?
if there is a chance to get rid of those, go ahead and try. Perhaps
they play a role for numerals and natural numbers, but this is just a
suspicion.
Cheers
Florian
--
Home:
Is there any good reason why the constants neg and iszero (defined
in Int.thy) are needed anymore?
Currently they are used to simplify (in)equalities on numerals; for
example, number_of x number_of y rewrites to neg (x + - y).
However, Int.thy also provides separate sets of rules like
