Re: [isabelle] tactic being executed twice



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.

Cheers
Lars




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