[isabelle-dev] Numeral simplification: neg and iszero

[Tobias Nipkow]

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