[isabelle] Feature wish: Minimal simp/auto invocations



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

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?

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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