[isabelle] Loose bound variable



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

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.