On Sat, 29 Oct 2011, Brian Huffman wrote:
Lately I have been trying to clean up the code of the cancellation
simprocs, and I have come across something I don't understand.
I welcome this effort. Many of the simprocs go back to early experiments
of myself and Larry in the mists of time. I have lost any account of how
they work, so whatever you find out, you are welcome to take care of it.
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 first thinking of Larry, but this is a rather new one by Tobias,
from just 2.5 years ago.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
