[isabelle-dev] HOL-IMP very slow

[Makarius]

On Thu, 13 Feb 2014, Jasmin Blanchette 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 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