[isabelle-dev] Why do cancellation simprocs call Lin_Arith.simproc
Brian Huffman
brianh at cs.pdx.edu
Sat Oct 29 09:22:27 CEST 2011
Hello all,
Lately I have been trying to clean up the code of the cancellation
simprocs, and I have come across something I don't understand.
One set of simprocs will cancel factors from inequalities, rewriting
terms like "x * z < y * z" to either "x < y" or "y < x", depending on
whether it can prove "0 < z" or "z < 0". What I don't understand is
the method they use to try to prove "0 < z" or "z < 0": Instead of
recursively calling the full simplifier (as the simplifier would do
when applying a conditional rewrite rule) it just calls the linear
arithmetic simproc directly. (The code for this is in the function
sign_conv in HOL/Tools/numeral_simprocs.ML, introduced in rev.
57753e0ec1d4.)
This necessitates some awkward/redundant setup of simp rules: For
example, at type real, we have the cancellation simprocs, which match
goals like "x * z < y * z" or "z * x < z * y". We also have some
cancellation simp rules like "0 < z ==> (z * x < z * y) = (x < y)". It
seems like the simprocs should make the simp rule redundant, but they
don't: Terms like "real (fact n) * x < real (fact n) * y" can be
rewritten by the simp rule, but the simproc fails because it cannot
solve the side-condition "0 < real (fact n)".
Is there any reason why the cancellation simprocs *shouldn't* call the
full simplifier recursively?
- Brian
More information about the isabelle-dev
mailing list