Okay, I see that this works the same as before. Such brittleness is quite believable, but is a sign that the particular proof was fragile anyway (having a large search space and requiring luck to get a solution quickly).
Larry On 13 Feb 2014, at 12:41, Jasmin Blanchette <[email protected]> wrote: > Am 13.02.2014 um 13:35 schrieb Lawrence Paulson <[email protected]>: > >> 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 > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
