[isabelle-dev] Numeral simplification: neg and iszero
Brian Huffman
brianh at cs.pdx.edu
Wed Dec 3 07:48:48 CET 2008
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
More information about the isabelle-dev
mailing list