Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]

On Fri, 4 Oct 2013, Christoph LANGE wrote:

2013-10-04 10:42 Makarius:
With the implicit "auto sledgehammer" and explicit "slegdehammer panel"
you normally don't put query commands in the buffer anymore,

Could you once more explain what "auto sledgehammer" is?  I know
entering "sledgehammer" (or "try", which I use in practice most of the
time) into the buffer, and I know the new sledgehammer panel, and I
didn't see anything else in the NEWS file.

The NEWS file has this very terse entry:

  * Support for automatic tools in HOL, which try to prove or disprove
  toplevel theorem statements.

The sledgehammer manual then has this:

  For Isabelle/jEdit users, Sledgehammer provides an automatic mode that
  can be enabled via the “Auto Sledgehammer” option under “Plugins > Plugin
  Options > Isabelle > General.” In this mode, Sledgehammer is run on
  every newly entered theorem.

The Plugin Options have more "automatically tried tools" in store, most of them off by default.

"Auto methods" is the same mechanism as 'try0', but it tends to suck up a lot of CPU resources, since the classic Isabelle proof tools easily get into non-terminating situations without instrumentation by facts that are properly classified as simp/intro/elim/dest/iff.

I should probably say a few more general things about the "auto" tools in the still empty slots of the jedit manual, pointing to the other manuals, too.

We also need more practical experience with such options.


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