Email Gateway (Aug 19 2022 at 12:06): Email Gateway (Aug 19 2022 at 12:06):From: René Thiemann <rene.thiemann@uibk.ac.at>
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
Last updated: Apr 25 2024 at 08:20 UTC