Re: [isabelle] Unexpected Sledgehammer behaviour

Hi Lars-Henrik,

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

I have to deeper knowledge of sledgehammer, but for the simplifier
»using P by simp« and »by (simp add: P)« makes a substantial difference.
 From what you report I would guess that sledgehammer tries to find
rules to add to the simplifier »simp add: …« rather than facts to extend
to proof scope »using …«.   Maybe an expert on sledgehammer can comment
on this.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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