Re: [isabelle] tactic being executed twice

Hi Lars,

Thanks - it seems from what you are saying as implying that a tactic shouldn't raise an exception even when applied to the wrong goal. Anyhow proceeding this way has solved the problem, thanks.

Also, using CSUBGOAL works.  I couldn't understand
what "Subgoal.FOCUS" does. CSUBGOAL is similar to SUBGOAL which is described clearly in the old Reference Manual.



On 06/06/2018 12:54 AM, Lars Hupel wrote:
Hi Jeremy,

At this point it seems clear that the tactic is executed twice, the
first time seemingly with an argument thm which gets printed out as
"TERM _", and the second time with the actual goal state.

this is a static check. The NEWS entry says:

* More static checking of proof methods, which allows the system to
form a closure over the concrete syntax.  Method arguments should be
processed in the original proof context as far as possible, before
operating on the goal state.  In any case, the standard discipline for
subgoal-addressing needs to be observed: no subgoals or a subgoal
number that is out of range produces an empty result sequence, not an
exception.  Potential INCOMPATIBILITY for non-conformant tactical
proof tools.

Essentially, this check is trying to figure out whether or not a proof
method (in your case: tactic) observers some discipline.

In my experience, the easiest way to make a tactic conform is to use the
various "Subgoal.FOCUS" combinators that are described in §6.3 of the
implementation manual. ("SUBGOAL" works too, it is a bit more low-level.)

Why is this?  What's going on here?  Is this how apply tactic ... should
be used?

When wrapped in the combinators I've mentioned, you don't have to worry
about these details.


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