[isabelle-dev] Fwd: [isabelle] Exception in conv.ML

[Lawrence Paulson]

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 <andreas.lochbihler at kit.edu>
> Date: 27 May 2011 14:51:27 GMT+01:00
> To: isabelle-users <isabelle-users at cl.cam.ac.uk>
> 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: andreas.lochbihler at kit.edu
> http://pp.info.uni-karlsruhe.de
> KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft
>