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 MHonArc.