[isabelle-dev] HOL-IMP very slow

[Jasmin Blanchette]

Am 13.02.2014 um 13:35 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:

> 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.

All I'm trying to say is that

    lemma "n ~= Suc n"
    using [[metis_trace]] by (metis Suc_n_not_n)

and

    lemma "x ~= Suc x"
    using [[metis_trace]] by (metis Suc_n_not_n)

generate slightly different clauses at the Metis level, as can be seen in the trace. One gets

    |- v_n = c_Nat_OSuc v_n

vs.

    |- v_x = c_Nat_OSuc v_x

To Metis, "v_n" and "v_x" are nullary function symbols (constants). Some of its heuristics are influenced by the concrete names, or at least their relative ordering. So it mgiht be very fast on the first one and very slow on the second one.

Jasmin