Re: [isabelle] Strange Behaviour of ALLGOALS



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


Am 06.04.2009 um 01:02 schrieb Jeremy Dawson:

Burkhart Wolff wrote:
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*}



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









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