[isabelle-dev] Numeral simplification: neg and iszero
Quoting Tobias Nipkow nipkow at in.tum.de: 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 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. - Brian
[isabelle-dev] Numeral simplification: neg and iszero
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. The rules in Tools/ComputeNumeral.thy are used within ML code for the HOL computing oracle. It's true, they are basically a cleaned up version of the NatBin.thy rules; simplification with these rules is supposed to work together with the oracle, not necessarily with the simplifier. Changes here might break my part of the proof of the Kepler Conjecture; but chances are it does not run with the current version of Isabelle anyway :-) Steven
[isabelle-dev] Numeral simplification: neg and iszero
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.
[isabelle-dev] Numeral simplification: neg and iszero
I would agree that changing simp rules to avoid using neg is not a huge improvement in and of itself. At best, it can reduce the number of rewrite steps needed to solve some arithmetic subgoals. However, speeding up simplification was not my primary goal. I share the opinion of Makarius that we would be much better off with numerals based on the natural numbers, rather than the integers. This would let us have a nice, clean way of doing arithmetic on arbitrary semirings - the ad-hoc, ugly, and inefficient rewrite rules in NatBin would no longer be needed. I think that the transition to nat-based numerals will be facilitated by cleaning up the simplification rules for arithmetic, and removing any unnecessary uses of subtraction (e.g. less_number_of_eq_neg and friends). - Brian Quoting Lawrence Paulson lp15 at cam.ac.uk: 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