[isabelle-dev] Numeral simplification: neg and iszero

[Brian Huffman]

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 this:

lemma less_int_code [code]:
   "Int.Pls < Int.Pls \<longleftrightarrow> False"
   "Int.Pls < Int.Min \<longleftrightarrow> False"
   "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
   "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
   "Int.Min < Int.Pls \<longleftrightarrow> True"
   "Int.Min < Int.Min \<longleftrightarrow> False"
   "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
   "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
   "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
   "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
   "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
   "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
   "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
   "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"

These are declared with the [code] attribute; wouldn't they also work  
just as well as simp rules? It seems that the old rewrite strategy  
using "neg" and "iszero" was designed to minimize the total number of  
rewrite rules in the simp set; I'm not sure whether this was done for  
performance reasons, or just for the fact that it was easier to  
implement, because there were fewer lemmas to prove.

I would propose that we change the simplification strategy for  
(in)equalities on numerals to use the code lemmas instead, and  
completely get rid of "neg" and "iszero". I think the code lemmas are  
cleaner and easier to understand, and they will also make the  
transition to unsigned numerals easier (since we no longer need to  
rely on subtraction to do comparisons).

- Brian