Re: [isabelle] Strange Behaviour of ALLGOALS



On Thu, 2 Apr 2009, Burkhart Wolff wrote:

I encountered a strange behaviour of ALLGOALS under
Isabelle/HOL 2008.

 apply(tactic "ALLGOALS(COND' contains_eval thyp_ify (K all_tac))")

results in the error message:

*** Unknown context
*** At command "apply".


while each individual call:

 apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 4")
 apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 3")
 apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 2")
 apply(tactic "(COND' contains_eval thyp_ify (K all_tac)) 1")

works fine.

According specification in tctical.ML, they should behave the same ...

These tactic invocations should be functionally the same, but the exact internal evaluation behaviour is different. The version without ALLGOALS can potentially run a bit further, and probably peeks at the implicit context that is still active during compilation of the "tactic" expression. Later at actual runtime this is no longer available, and produces the "Unknown context" error.

Neither ALLGOALS nor COND' are at fault here. You should look at contains_eval thyp_ify instead at figure out where the context is accessed, e.g. via the_context() or simpset() or similar. All of this belongs to old layers of the system and is more and more at retreat. Usually it is best to refer to the context explicitly, passing through ctxt: Proof.context where required and provide that value in the very end via the @{context} antiquotation. E.g. like this:

ML {*
  fun my_tac ctxt i = ...
*}

...
  apply (tactic "ALLGOALS (my_tac @{context})")


	Makarius





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