On Thu, 13 Feb 2014, Jasmin Blanchette wrote:
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 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.
The Subgoal.FOCUS combinator turns goal parameters into local fixes of the
context, re-using the accidental "comment" fields in the Abs nodes, in the
traditional way "as they are printed" (this is a well-known insider joke).
What I have explained before about the reasons to use Variable.next_bound
in the Simplifier seems to apply here as well. So I should probably try
the same in these structured proof combinators, but the formerly adhoc
"bounds" of the Simplifier need a few more reforms first, to make them
actual fixes.
In any case, such a change of internal names is likely to break existing
proofs and proof tools, but this needs concrete empirical exploration
instead of speculation.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
