# [isabelle-dev] HOL-IMP very slow

Makarius makarius at sketis.net
Wed Feb 12 19:40:01 CET 2014

```On Wed, 12 Feb 2014, Jasmin Christian Blanchette wrote:

> Am 12.02.2014 um 16:40 schrieb Dmitriy Traytel <traytel at in.tum.de>:
>
>> Should be fine again (or at least better) with b445c39cc7e9. Thanks for

OK, everything back to normal.

> For the record: The goal state before and after had different variable
> names in it. These become Skolem constants to Metis (in the FO logic
> sense, not in the Isabelle sense). The Metis prover, like most if not
> all ATPs, is sensitive to the (relative order of the) names of the
> symbols -- e.g. it may apply different rules in a different order.
>
> It would be possible, and indeed a good idea, to insulate ourselves from
> this by having the "metis" proof method name Skolems serially ("sk1",
> "sk2", etc.) before invoking the Metis prover [*]. This would probably
> trigger a couple of bad cases like we saw today, but as a result we
> would be immune from the disease.

In principle the concept of "bound" variable in the context can do that,
that the usual term order (the one of the Simplifier) coincides with the
enumeration order.

The context also takes care to print these frees in green, as if they were
actual bounds under a lambda.  (I have recently made this a general
principle, not just some special hack of the Simplifier to print terms
privately.)

Here is an example:

ML {*
val ctxt = @{context};
val xs =
replicate 100 ()
|> map (fn _ => ("x" ^ string_of_int (random_range 1 100), @{typ 'a}));

val (xs', ctxt') = fold_map Variable.next_bound xs ctxt;

val x = hd xs;
val x' = hd xs';
writeln (Syntax.string_of_term ctxt' (Free (x', snd x)))
*}

So for the user, the original names are mostly preserved (according to the
insider joke "as they are printed"), while for the system the row of names
is always in a standard form.

This mechanism was originally introduced for the Simplifier, to go under
abstractions in a robust manner.  (When it was introduced it was actually
not that robust, and broke down for > 255 names, as discovered by David
von Oheimb when he did the first version of Bali.)

Name.is_bound is used to detect these funny pseudo-bounds -- excactly once
in hypsubst.ML that is probably irrelevant here.  (Although hypsubst is
also open to surprises as we now know.)

> Metis is a FO ATP developed by Hurd. "metis" is a higher-order proof
> method (and tactic) that translates HOL to FOL (like Sledgehammer does),
> developed by Paulson & Susanto.

Do you understand yourself how that works?

Makarius

```