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,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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