# [isabelle-dev] Numeral simplification: neg and iszero

Brian Huffman brianh at cs.pdx.edu
Tue Dec 9 17:40:22 CET 2008

```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 give a progress report on my efforts to get rid of
iszero and neg.

For simplification of inequalities of numerals in class
{number_ring,ordered_idom}, getting rid of neg was indeed simple. The
old rules were

less_number_of_eq_neg: "number_of x < number_of y <--> neg (number_of
(x + - y))"
le_number_of_eq: "number_of x <= number_of y <--> ~ neg (number_of (y + - x))"

The new rules are

less_number_of: "number_of x < number_of y <--> x < y"
le_number_of: "number_of x <= number_of y <--> x <= y"

Fortunately, the new rules hold in the same class
{number_ring,ordered_idom} as the old ones. The same is not true for
testing equality, however. The original rule is

eq_number_of_eq:
"(number_of x::'a::number_ring) = number_of y <--> iszero (number_of
(x + - y)::'a)"

I wanted to replace this with

eq_number_of:
"(number_of x::'a::{number_ring,ring_char_0}) = number_of y <--> x = y"

But as you can see, eq_number_of has an additional class constraint
requiring that of_int be injective, while eq_number_of_eq works in any
number ring. Since the iszero function is polymorphic, this lets us
solve numeral equalities on, for example, word types (where of_int is
not injective) by defining special simp rules for iszero at those
types. Even without any additional simp rules, eq_number_of_eq can be
used to prove inequalities like -1 ~= 0 or 5 ~= 6 at any number_ring
instance (since 1 is required to be nonzero in every unital ring). Any
replacement for eq_number_of_eq must still be able to solve such
subgoals.

I did try modifying eq_number_of_eq to use subtraction, replacing (x +
- y) with (x - y). But subtraction on the binary representation causes
another problem: We would like to rewrite (Int.Min - Int.Min) to
Int.Pls, but the simplifier rewrites this to (0::int) instead, leaving
us with ill-formed terms like "number_of (Int.Bit0 (0::int))". For
these reasons, I have left eq_number_of_eq in its original form, and
iszero will stay (at least for now).

I do think that we can get rid of "neg". The other place where "neg"
was used a lot was in NatBin.thy, for simplifying binary arithmetic at
type nat. I replaced many occurrences of "neg (number_of v::int)" with
"v < Int.Pls"; I also simplified more awkward constructions like "neg
(number_of (- v))" to "Int.Pls < v", and "neg (number_of v::int) |
iszero (number_of v::int)" to "v <= Int.Pls".

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 made redundant, or merged into
NatBin.thy, then we will be able to remove "neg".

- Brian

```