Am 13.02.2014 um 13:19 schrieb Lawrence Paulson <l...@cam.ac.uk>:
> I’m not sure what the question is any more. If it is about the choice of
> names in Skolemization, that has been entirely redone in the past few years.
> I imagine it is now something like this:
>
> Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
> EVERY1 [skolemize_prems_tac ctxt negs,
> Subgoal.FOCUS (cltac o mkcl o #prems) ctxt'])
> ctxt 1]) i st
>
> (I found this in meson.ML.)
>
> The original version made little use of contexts, as I recall.
I was a bit confused when I wrote about "skolemization" being the culprit. The
problem is that fixed variables occurring in the conjecture end up keeping
their names (modulo some slight alterations). After all, such variables are for
all practical purposes just like constants. By "fixed" variables, I mean among
other things the "parameters" of the goal (those entites which "rename_tac"
works on).
That "metis" performance is affected by the naming of constants is not
surprising to anybody who knows a thing or two about automated reasoning, but
it is surprising that even the goal parameter naming affects it.
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
