[isabelle-dev] Numeral simplification: neg and iszero

[Brian Huffman]

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