Email Gateway (Aug 18 2022 at 14:36): Email Gateway (Aug 18 2022 at 14:36):From: Stefan Berghofer <berghofe@in.tum.de>
Hi Andreas,
thanks for reporting this problem. The exception was caused by a bug in
(r)trancl_tac, which is installed in the simpset as a solver. I have fixed
this in the repository version of Isabelle, see
http://isabelle.in.tum.de/repos/isabelle/rev/206e2f1759cc
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 14:47):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello,
I wanted to prove a lemma with an apply script. After some manipulations
(induct, rule, drule, frule) of the goals, auto, fastsimp or force
should easily solve the remaining goal. However, simp (and all methods
that use the simplifier) produce only this error message:
*** exception TYPE raised (line 341 of "sign.ML"): Loose bound variable: B.4
*** At command "apply".
What does this error message mean? And how can I avoid it? Is there
something wrong with my simplifier setup?
The complete exception trace (with debugging turned on) is below.
Regards,
Andreas
Exception trace for exception - TYPE raised in sign.ML line 341
Sign.type_check(2)typ_of(2)
Sign.type_check(2)typ_of(2)
Sign.type_check(2)typ_of(2)
Sign.type_check(2)typ_of(2)
Sign.type_check(2)
Sign.certify'(1)(1)(1)(1)(1)(1)
Trancl_Tac().prove(3)inst(1)
Trancl_Tac().prove(3)pr(1)
List.map(2)
Trancl_Tac().rtrancl_tac(1)(2)(1)(6)
Subgoal.GEN_FOCUS(5)
Trancl_Tac().rtrancl_tac(1)(2)(1)
Tactical.ORELSE(1)(1)
Tactical.ORELSE(1)(1)
Seq.map(2)(1)
Seq.flat(1)(1)
Seq.filter(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Toplevel.proofs'(1)(1)(1)
Runtime.debugging(2)(1)
End of trace
proof (prove): step 7
fixed variables: final, r, t, s, was, s'
prems:
rtrancl3p (redTW t) s was s'
Suspend ?w \<notin> set was
goal (1 subgoal):
1. \<And>a bs a' b a''.
\<lbrakk>rtrancl3p (redTW t) a bs a'; redTW t a' b a'';
\<And>w. Suspend w \<notin> set (bs @ [b]);
(interrupted_mem_red (thr a) (wset a))\<^sup>*\<^sup>* (shr a')
(shr a'');
(interrupted_mem_red (thr a) (wset a))\<^sup>*\<^sup>* (shr a)
(shr a')\<rbrakk>
\<Longrightarrow> (interrupted_mem_red (thr a) (wset
a))\<^sup>*\<^sup>* (shr a) (shr a'')
*** exception TYPE raised (line 341 of "sign.ML"):
*** Loose bound variable: B.4
*** B.4
*** At command "apply".
Email Gateway (Aug 18 2022 at 14:48):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
I wanted to prove a lemma with an apply script. After some
manipulations (induct, rule, drule, frule) of the goals, auto,
fastsimp or force should easily solve the remaining goal. However,
simp (and all methods that use the simplifier) produce only this
error message:*** exception TYPE raised (line 341 of "sign.ML"): Loose bound
variable: B.4
*** At command "apply".What does this error message mean?
Isabelle's internal representation of lambda-terms uses de Bruijn
indices for bound variables. Errors like these usually mean that
there's a rather bad bug in some code that directly manipulates term
(e.g., some code that removes a lambda abstraction forgot to decrement
te bound variable indices).
And how can I avoid it? Is there something wrong with my simplifier
setup?
Is there anything _special_ about your simplifier setup?
Jasmin
Email Gateway (Aug 18 2022 at 14:48):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Please do. There wasn't much to be learned by just looking at the trace.
Jasmin
Email Gateway (Aug 18 2022 at 14:48):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Jasmin,
thank you for the explanation.
No, not really. I have added some lemmas to the simp set, but that's
about all. In particular, I haven't written any simpprocs.
If you like, I can send you my Isabelle2009-1/HOL theories such that you
can reproduce the error and try to find bug.
Andreas
Last updated: Apr 26 2024 at 04:17 UTC