[isabelle-dev] Numeral simplification: neg and iszero
Lawrence Paulson
lp15 at cam.ac.uk
Tue Dec 9 18:02:43 CET 2008
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".
More information about the isabelle-dev
mailing list