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

[Makarius]

On Thu, 9 Jun 2011, Lawrence Paulson wrote:

> I see you are alert, as always!

Just the normal process of consuming incoming mails and changesets ... :-)

But here there were two reasons for extra attention: (1) suspicious 
keywords in the log entry (like "fixed" or "bug") and (2) a realistic 
chance that I broke this myself in recent reworking of blast (a relatively 
simple case of the still ongoing "localisation" effort).


> In this particular case, it's pretty clear that the exception was raised 
> here, in conv.ML:
>
> fun gconv_rule cv i th =
>  (case try (Thm.cprem_of th) i of
>    SOME ct =>
>      let val eq = cv ct in
>        if Thm.is_reflexive eq then th
>        else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
>      end
>  | NONE => raise THM ("gconv_rule", i, [th]));
>
> And this was in conformance with a common use of exception THM, namely 
> to indicate that the designated subgoal did not exist. So a tactic 
> calling this code should indeed catch the exception and indicate failure 
> by returning the empty sequence.

Yes, formally timing_depth_tac was always wrong in that sense as a tactic. 
I have learned the requirements for proper tactics from you many years ago 
(they are now documented in the implementation manual).  Normally the 
CONVERSION tactical would convert the failure of the conversion (e.g. via 
exception THM) into proper Seq.empty for the tactic, but it was not used 
here for other reasons.

Just some weeks ago I inspected the code again, and convinced myself that 
the DEEPEN around timing_depth_tac "repairs" this feature.  Unfortunately 
I've overlooked the special side-entry Blast.depth_tac, which bypasses 
DEEPEN.  So historically the problem was actually introduced in 1997 here 
http://isabelle.in.tum.de/repos/isabelle/rev/cc3e8453d7f0 when the public 
Blast.depth_tac was added as new feature.


> Did anybody actually understand the source of the problem?

In summary the situation is like that: blast with explicit depth limit did 
not check subgoal bounds properly.  The problem can be reproduced like 
that (e.g. in Isabelle2011):

   lemma True
     apply rule
     apply (blast 5)

*** exception THM 1 raised (line 212 of "conv.ML"): gconv_rule
*** At command "apply" (line 7 of "/home/makarius/Scratch.thy")

Without that extra argument it is deepened from 1 .. 20.  Since Andreas 
had explicit 25 to get beyond that, he might consider using 
[[blast_depth_limit = 30]] or similar to get the incremental effect to 
higher limits, although there could be a general slowdown up there.


See also http://isabelle.in.tum.de/repos/isabelle/rev/01f051619eee for 
some further cleanup of blast.


 	Makarius