[isabelle-dev] Numeral simplification: neg and iszero

[Lawrence Paulson]

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

On 9 Dec 2008, at 16:40, Brian Huffman wrote:

> 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".