Re: [isabelle] Simplifier: renamed bound variable ":000" to ":000a"
On Wed, 17 Feb 2010, Brian Huffman wrote:
Sometimes the simplifier produces a warning message that looks like this:
### Simplifier: renamed bound variable ":000" to ":000a"
Should I care?
If it is important, what does this message mean---does it indicate a problem?
If it is *not* important, why is this message printed at all? (Or at
least, why is it printed even when the debugging flag is not turned on?)
This message indicates a situation where some Simplifier component
(simproc, looper, solver, or similar) does not observe the proof context.
When simplifying abstractions, fresh variables need to be invented -- the
"bounds" part of the simpset records already used auxiliary variables.
Sometimes this information is lost, because some tool restarts
simplification in an empty context (in ancient days tools could work from
the background theory alone). The Simplifier is smart enough to detect the
clash and tries to repair it, which appears to work in most situations.
At some point I would like to see these remaining holes in existing proof
tools being filled. Although there is no immediate problem, this is a bit
strange -- just like plugging the power cord to switch off a computer
instead of a clean shutdown.
This archive was generated by a fusion of
Pipermail (Mailman edition) and