> 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.)
I was probably afraid of an excessive number of recursive simplifier calls in the case of long products. But that is not a killer argument. Just try it. Tobias > 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 > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
