[isabelle-dev] HOL-IMP very slow

[Lawrence Paulson]

I know it was a problem for machine learning that a free variable in a goal (x say) might appear with multiple types in a problem set. This is connected with the issue you’re describing now. I assume that that was solved somehow.
Larry

On 13 Feb 2014, at 12:31, Jasmin Blanchette <jasmin.blanchette at gmail.com> wrote:

> Am 13.02.2014 um 13:19 schrieb Lawrence Paulson <lp15 at 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
>