[isabelle-dev] [isabelle] Problem "exception TYPE raised: Loose bound variable"

[Lawrence Paulson]

It makes sense to move this discussion to the developers' list, as it concerns the release candidate.

In an attempt to get to the bottom of this problem a little, I applied a series of single-step commands, resulting in an expression that is almost legible. Simplifying this expression yields the same exception. However, one further command (removing the surrounding expression "%u. add_vars_sum (vas, u)") eliminates the error.

The entire proof can also be done in a single line by the command

	apply (simp cong del: if_cong) 

So I am guessing that the bug lies within the congruence solver.

I hope that these clues will allow somebody to get to the bottom of it.

Larry Paulson
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2013-10-15 at 15.37.18.png
Type: image/png
Size: 328812 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131015/2cc20d08/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.thy
Type: application/octet-stream
Size: 4216 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131015/2cc20d08/attachment-0001.obj>
-------------- next part --------------

On 15 Oct 2013, at 10:45, René Thiemann <rene.thiemann at uibk.ac.at> wrote:

> Dear all,
> 
> recently I stumbled upon an "Loose bound variable" exception in "sign.ML".
> 
> The problem occurred when I wanted to show that a certain operation is
> invariant under record-updates.
> 
> If I do the proof incrementally (first proving invariance for all the auxiliary 
> functions), then everything works fine. However, doing the same kind of reasoning
> directly without explicitly considering the auxiliary functions, then calling the
> simplifier led to the above exception.
> 
> The problem occurs in both Isabelle2013-RC2 and in the development version
> (80660c529d74)
> 
> I just want to report this problem, a small theory file is attached.
> I tried to simplify the example as much as possible, but several further 
> simplification which I tried resulted in normal behavior without the exception.
> 
> Kind regards,
> René
> 
> <Test.thy>