[isabelle-dev] Why do cancellation simprocs call Lin_Arith.simproc
makarius at sketis.net
Sat Oct 29 12:53:58 CEST 2011
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.
I was first thinking of Larry, but this is a rather new one by Tobias,
from just 2.5 years ago.
More information about the isabelle-dev