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
Brian Huffman schrieb:
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
___
Isabelle-dev mailing list
Isabelle-dev at mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
