[isabelle] Disable proof automation locally, per theorem?



Hi all,

for a test I have enabled all "auto" proof tools in
Isabelle2013-1-RC1/jEdit and I like it so far.

There is just one minor annoyance that makes me lose track of my
progress in maintaining my formalisation:

The blue (i) notification that an automated proof has been found is
always displayed, even if exactly that proof is already in place.

E.g. if I have

lemma foo: "..." by blast

and the auto tools find out that "by blast" is the best proof, they
notify me of this.  Now, implementing some functionality that would
automatically hide the notification in such cases probably wouldn't make
sense, as the "fastest" proof method depends a lot on the context
(characteristics of my machine, cache, etc., I guess), and as there is
not always a unique fastest method.

However, I would really find it useful if there were a way of manually
and selectively suppressing such notifications, or actually locally
disabling automation.  That is, I would generally like to see them, but
when I think that lemma foo above already has the best possible proof, I
don't want a blue (i) to grab my attention.  I would only want to see
this notification on proof steps I have not yet reviewed.

Cheers,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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