Re: [isabelle] Feature wish: Minimal simp/auto invocations



Am 16/11/2012 23:25, schrieb Joachim Breitner:
> Dear Isabelle users (and devs, I guess),
> 
> I am using sledgehammer/metis more and more even for very simple and 
> obvious lemmas that I could mostly also solve with simp or auto. The great
> thing about sledgehammer is that it searched a proof taking many lemmas
> into account, but then produces a command that explicitly mentions the
> lemmas that are required, which is very useful feedback to me, and helps,
> for example, in refactoring.
> 
> Is there a chance to get a similar feature for the simplifier? I could 
> imagine that when I write apply (simp minimize add: foo) the simplifier
> would run as usual, but it would also keep track of which simplification
> rules were actually used.

We are planning to provide a much improved tracing facility for the simplifier
which will certainly keep track of such things and will tell you, for example,
if a rule you added explicitly was not used at all. We could also provide the
list of all rules used.

> The output window would then say something along the lines simplification
> used 5 lemmas. Use "apply (simp only: foo bar baz bam bang)" (12ms) to 
> reproduce. and in the IDE I could click on that to replace the original
> invocation with this more explicit command.

I doubt we want to go down that route. The simplifier often uses lots of
rules, which would lead to a very long list if supplied explicitly, which is
ugly. Moreover it would expose information we want to hide: how exactly a lot
of basic computations are organized, especially rewriting on numbers. Your
suggestion would create simplifier calls that hardwire that information and
make such steps very brittle under change. I don't want to encourage that.

> It could work similarly (but maybe harder to implement, I presume) for 
> auto.
> 
> 
> More generally, as I’m basically working with Isabelle fulltime these days,
> there are more usability improvement ideas cropping up. Is this the right
> forum and form to suggest them?

It is, thanks.

Tobias


> Greetings, Joachim
> 





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