[isabelle] Unexpected Sledgehammer behaviour



Dear list,

Consider this lemma:

lemma assumes "rel_set R (insert C {}) (insert D {})" and "R A B"
        shows "rel_set R (insert A (insert C {})) (insert B (insert D {}))"

"sledgehammer" produces this best proof: by (smt assms(1) assms(2) insert_iff rel_set_def)

while "using assms sledgehammer" produces this best proof: by (simp add: rel_set_def)

This difference surprises me. The Sledgehammer User's Guide doesn't mention that "using" has any effect other than directing the selection of relevant facts -- but Sledgehammer selected the facts needed by the second proof also without "using" -- as they were used in the first proof.

Are there any other effects of "using" in this context?

Lars-Henrik

Lars-Henrik Eriksson, Computing Science, Dept. of Information Technology, Uppsala University, Sweden





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.