I'll be happy to provide a trace if you tell me how to obtain one. If I turn on
"Debugging" in the settings menu, I only get an empty exception trace in the
isabelle buffer:
Exception trace for exception - THM raised in conv.ML line 212
End of trace
Andreas
Lawrence Paulson schrieb:
It looks like this exception is raised when gconv_rule cv i th is called and
the specified subgoal does not exist. The function gconv_rule is called in only
four places in Pure:
./Isar/element.ML: (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
./raw_simplifier.ML: then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
./raw_simplifier.ML: Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE
o prover_tac) ss) i thm)
./tactical.ML:fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
Without a full trace, it is impossible to be certain which one. I looked in
raw_simplifier.ML, and the two calls did the necessary check to prevent this
exception from being raised. The function CONVERSION in tactical.ML does no
check, but catches exception THM. This leaves the function compose_witness in
Isar/element.ML, where I see neither a check that the subgoal exists nor an
exception handler. But I could be wrong, as such checks may be done elsewhere.
Does anybody else have a suggestion?
Larry
Begin forwarded message:
From: Andreas Lochbihler <[email protected]>
Date: 27 May 2011 14:51:27 GMT+01:00
To: isabelle-users <[email protected]>
Subject: [isabelle] Exception in conv.ML
Hi all,
have the following weird behaviour. After having applied auto on my goal, I am
left with 24 subgoals. Applying 24 copies of the following invokation of the
blast method solves all 24 subgoals. However, if I try to collaspe all of them
into a single invokation apply(blast 25 ...)+, I get the exception below.
What is going wrong here? And how can I fix it?
If need be, I can make my theories available, but I doubt that I can produce a
minimal core example.
apply(blast 25 intro: rtranclp_trans rtranclp_tranclp_tranclp
treds1r_cons_treds1r List1Red2 treds1t_cons_treds1t
dest: t)
*** exception THM 1 raised (line 212 of "conv.ML"):
*** gconv_rule
*** EX es'' xs''.
*** P,e # es,n,h' |- (es'', xs'') [<-->] (stk', loc', pc', xcp') &
*** (if tmoves2 (compP2 P) h stk (e # es) pc xcp
*** then h' = h &
*** (if xcp' = Any --> pc < pc' then treds1r else treds1t) P t h
*** (e' # es, xs) (es'', xs'')
*** else EX ta' es' xs'.
*** treds1r P t h (e' # es, xs) (es', xs') &
*** P,t |- <<es',(h, xs')>> [-ta'->] <<es'',(h', xs'')>> &
*** ta_bisim wbisim1 (extTA2J1 P ta') ta &
*** ¬ tmoves1 P h es' &
*** (calls1 (e' # es) = None &
*** no_calls2 (e # es) pc & es' = e' # es & xs' = xs))
*** At command "apply"
Best regards,
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: [email protected]
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: [email protected]
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
