Re: [isabelle] Auto sledgehammer on completed lemmas



> I've noticed after enabling auto-Sledgehammer that it (and friends like Nitpick) run on all the
> lemmas in any file you open. So, for example, when you open a previously worked on theory,
> Sledgehammer starts attacking lemmas that already have completed proofs. This isn't a large
> impediment, but I just wanted to suggest that perhaps this behaviour could be improved on in future
> by noticing the completed proof.

There is actually a good use for this in some cases: autosledgehammer is extremely good at pointing out redundant lemmas.

Going through larger proof updates recently, I was able to remove quite a few proofs that were duplicates or close duplicates, which autosledgehammer had highlighted for me.

So maybe this should be configurable, at least.

Ideally autosledgehammer would recognise lemmas that are already solved by a one-liner and always skip those. And autosolve skip those that are already solved by a single rule application with one of the rules it is suggesting. But thatâs probably a lot of proof text analysis for something that doesnât really want to know about any of that.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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