Email Gateway (Aug 18 2022 at 13:18): Email Gateway (Aug 18 2022 at 13:18):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
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 ...
Can you help me?
bu
PS: In case that you need slightly more context
(but it should actually not matter):
ML{*
fun COND' C T1 T2 n = COND (C n) (T1 n) (T2 n);
fun contains_eval n thm =
let fun T("Natural.evalc",_) = true | T _ = false
in Term.exists_Const T (term_of(cprem_of thm n)) end*}
Email Gateway (Aug 18 2022 at 13:19):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 13:19):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Burkhart Wolff wrote:
Burkhart,
When I was using Isar I often found strange behaviour which was
something to do with theories, and I think the message *** Unknown
context suggests that this may be the case here also.
What behaviour do you get not using Isar, ie using the straight ML
interface, and
by (ALLGOALS(COND' contains_eval thyp_ify (K all_tac))) ;
by ((COND' contains_eval thyp_ify (K all_tac)) 4) ;
by ((COND' contains_eval thyp_ify (K all_tac)) 3) ;
by ((COND' contains_eval thyp_ify (K all_tac)) 2) ;
by ((COND' contains_eval thyp_ify (K all_tac)) 1) ;
?
Jeremy
Email Gateway (Aug 18 2022 at 13:20):From: Burkhart Wolff <bwolff@inf.ethz.ch>
Jeremy, thank you for your interest.
The problem is solved (thanks Makarius) : I used a construct
that makes reference to the proof-state
and binds the fixeds result somewhere inside a tactic.
(something equivalent to simpset(), but more
subtle: its 'thm "bla"', I guess 'theory "bla"' is the same ? ).
This kind of context violation is now rejected
much more strictly by the kernel than it was in
previous Isabelle versions.
The reason why the error pops up to surface at
the quite innocent ALLGOALS is somewhat
more obscure - but not really intereasting, I guess,
for this mailing list.
bu
Last updated: May 03 2024 at 08:18 UTC